Mercurial > cpdt > repo

comparison src/Intensional.v @ 189:0198181d1b64

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Automated CcExp_correct
author Adam Chlipala <adamc@hcoop.net>
date Mon, 17 Nov 2008 10:36:02 -0500
parents aec05464fedd
children cbf2f74a5130
comparison
equal deleted inserted replaced
188:aec05464fedd 189:0198181d1b64
1042 (forall t (v1 v2 : natvar t), In (existT _ _ (v1, v2)) G 1042 (forall t (v1 v2 : natvar t), In (existT _ _ (v1, v2)) G
1043 -> lookup_type v1 fvs = Some t) 1043 -> lookup_type v1 fvs = Some t)
1044 -> wfExp fvs e1. 1044 -> wfExp fvs e1.
1045 Hint Extern 3 (Some _ = Some _) => elimtype False; eapply lookup_bound_contra; eauto. 1045 Hint Extern 3 (Some _ = Some _) => elimtype False; eapply lookup_bound_contra; eauto.
1046 1046
1047 induction 1; crush. 1047 induction 1; crush; eauto;
1048 eapply H0. 1048 match goal with
1049 eauto. 1049 | [ H : _, envT : list Source.type |- _ ] =>
1050 1050 apply H with (length envT); my_crush; eauto
1051 apply H0 with (length envT). 1051 end.
1052 my_crush.
1053 eauto.
1054 Qed. 1052 Qed.
1055 1053
1056 Theorem Exp_wf : forall t (E : Source.Exp t), 1054 Theorem Exp_wf : forall t (E : Source.Exp t),
1057 wfExp (envT := nil) tt (E _). 1055 wfExp (envT := nil) tt (E _).
1058 intros; eapply Exp_wf'; 1056 Hint Resolve Exp_equiv.
1059 [apply Exp_equiv 1057
1060 | crush]. 1058 intros; eapply Exp_wf'; crush.
1061 Qed. 1059 Qed.
1062 End wf. 1060 End wf.
1063 1061
1064 Definition CcExp t (E : Source.Exp t) : Prog (ccType t) := 1062 Definition CcExp t (E : Source.Exp t) : Prog (ccType t) :=
1065 CcExp' E (Exp_wf E). 1063 CcExp' E (Exp_wf E).