proposition: Lemma check_aux_interp_aux_lt_aux : forall a h, (forall j : int, j <? h -> exists v : interp_t (v_type Typ.type interp_t (a .[ j])), a .[ j] = Bval (v_type Typ.type interp_t (a .[ j])) v) -> forall l, List.forallb (fun h0 : int => h0 <? h) l = true -> forall (f0: tval), exists v : interp_t (v_type Typ.type interp_t (let (tf, f) := f0 in apply_func (fst tf) (snd tf) f (List.map (get a) l))), (let (tf, f) := f0 in apply_func (fst tf) (snd tf) f (List.map (get a) l)) = Bval (v_type Typ.type interp_t (let (tf, f) := f0 in apply_func (fst tf) (snd tf) f (List.map (get a) l))) v.
proof: Proof. intros a h IH; induction l as [ |j l IHl]; simpl. intros _ [[[ | ] tr] f]; simpl. exists f; auto. exists true; auto. rewrite andb_true_iff; intros [H1 H2] [[[ |A targs] tr] f]; simpl. exists true; auto. destruct (IH j H1) as [x Hx]; rewrite Hx; simpl; case (Typ.cast (v_type Typ.type interp_t (a .[ j])) A); simpl. intro k; destruct (IHl H2 (Tval (targs,tr) (f (k interp_t x)))) as [y Hy]; simpl in Hy; rewrite Hy; simpl; exists y; auto. exists true; auto. Qed.
imports: Bool Int63 Psatz PArray BinNat BinPos ZArith SMT_classes_instances Misc State BVList