proposition: Lemma check_args_interp_aux : forall t l f, (let (targs, tr) := v_type Typ.ftype interp_ft f in check_args get_type l targs && Typ.eqb tr t) -> exists v : interp_t t, (let (tf, f0) := f in apply_func (fst tf) (snd tf) f0 (List.map interp_hatom l)) = Bval t v.
proof: Proof. intro A; induction l as [ |h l IHl]; simpl; intros [tf f]; simpl. destruct tf as [[ | ] tr]; try discriminate; simpl; rewrite Typ.eqb_spec; intro; subst tr; exists f; auto. destruct tf as [[ |B targs] tr]; try discriminate; simpl; rewrite <- andb_assoc; unfold is_true; rewrite andb_true_iff; change (Typ.eqb (get_type h) B = true /\ check_args get_type l targs && Typ.eqb tr A = true) with (is_true (Typ.eqb (get_type h) B) /\ is_true (check_args get_type l targs && Typ.eqb tr A)); rewrite Typ.eqb_spec; intros [H1 H2]; destruct (check_aux_interp_hatom h) as [v0 Heq0]; rewrite Heq0; generalize v0 Heq0; rewrite H1; intros v1 Heq1; simpl; generalize (IHl (Tval (targs,tr) (f v1))); simpl; intro IH; destruct (IH H2) as [v2 Heq2]; exists v2; rewrite Typ.cast_refl; auto. Qed.
imports: Bool Int63 Psatz PArray BinNat BinPos ZArith SMT_classes_instances Misc State BVList