Mercurial > cpdt > repo

comparison src/Intensional.v @ 188:aec05464fedd

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:31:22 -0500
parents 71c076dd5f31
children 0198181d1b64
comparison
equal deleted inserted replaced
187:71c076dd5f31 188:aec05464fedd
993 -> lr t (Source.expDenote e1) (Closed.expDenote (funcsDenote (ccExp e2 fvs wf) env)). 993 -> lr t (Source.expDenote e1) (Closed.expDenote (funcsDenote (ccExp e2 fvs wf) env)).
994 994
995 Hint Rewrite spliceFuncs_correct unpackExp_correct : cpdt. 995 Hint Rewrite spliceFuncs_correct unpackExp_correct : cpdt.
996 Hint Resolve packExp_correct lookup_type_inner. 996 Hint Resolve packExp_correct lookup_type_inner.
997 997
998 induction 1; crush. 998 induction 1; crush;
999 999 match goal with
1000 match goal with 1000 | [ IH : _, Hlr : lr ?T ?X1 ?X2, ENV : list Source.type, F2 : natvar _ -> _ |- _ ] =>
1001 | [ IH : _, Hlr : lr ?T ?X1 ?X2, ENV : list Source.type, F2 : natvar _ -> _ |- _ ] => 1001 apply (IH X1 (length ENV) (T :: ENV) (true, snd (fvsExp (F2 (length ENV)) (T :: ENV))))
1002 apply (IH X1 (length ENV) (T :: ENV) (true, snd (fvsExp (F2 (length ENV)) (T :: ENV)))) 1002 end; crush;
1003 end. 1003 match goal with
1004 1004 | [ Hlt : forall t v1 v2, _ -> _ < _, Hin : In _ _ |- _ ] =>
1005 crush. 1005 solve [ generalize (Hlt _ _ _ Hin); crush ]
1006 match goal with 1006 | [ |- context[match ?pf with refl_equal => _ end] ] => generalize pf
1007 | [ Hlt : forall t v1 v2, _ -> _ < _, Hin : In _ _ |- _ ] => 1007 end; simpl;
1008 generalize (Hlt _ _ _ Hin); crush 1008 match goal with
1009 end. 1009 | [ |- context[if ?E then _ else _] ] => destruct E
1010 1010 end; intuition; subst;
1011 crush; 1011 match goal with
1012 match goal with 1012 | [ |- context[match ?pf with refl_equal => _ end] ] => rewrite (UIP_refl _ _ pf); assumption
1013 | [ |- context[match ?pf with refl_equal => _ end] ] => generalize pf 1013 | [ Hlt : forall t v1 v2, _ -> _ < _, Hin : In (existT _ _ (_, length _)) _ |- _ ] =>
1014 end; simpl; 1014 generalize (Hlt _ _ _ Hin); crush
1015 match goal with 1015 | [ HG : _, Hin : In _ _, wf : wfExp _ _, pf : _ = Some _,
1016 | [ |- context[if ?E then _ else _] ] => destruct E 1016 fvs : isfree _, env : envOf _ _ |- _ ] =>
1017 end; intuition; subst; 1017 generalize (HG _ _ _ Hin (lookup_type_inner wf pf)); clear_all;
1018 try match goal with 1018 repeat match goal with
1019 | [ |- context[match ?pf with refl_equal => _ end] ] => rewrite (UIP_refl _ _ pf); assumption 1019 | [ |- context[match ?pf with refl_equal => _ end] ] => generalize pf
1020 | [ Hlt : forall t v1 v2, _ -> _ < _, Hin : In (existT _ _ (_, length _)) _ |- _ ] => 1020 end; simpl;
1021 generalize (Hlt _ _ _ Hin); crush 1021 generalize (packExp_correct _ fvs (inclusion wf) env pf); simpl;
1022 end. 1022 match goal with
1023 1023 | [ |- ?X == ?Y -> _ ] =>
1024 generalize (H2 _ _ _ H5 (lookup_type_inner wf pf)); clear_all. 1024 generalize X Y
1025 repeat match goal with 1025 end;
1026 | [ |- context[match ?pf with refl_equal => _ end] ] => generalize pf 1026 rewrite pf; rewrite (lookup_type_inner wf pf);
1027 end; simpl. 1027 intros lhs rhs Heq; intros;
1028 generalize (packExp_correct _ fvs (inclusion wf) env pf); simpl. 1028 repeat match goal with
1029 match goal with 1029 | [ H : _ = _ |- _ ] => rewrite (UIP_refl _ _ H) in *
1030 | [ |- ?X == ?Y -> _ ] => 1030 end;
1031 generalize X Y 1031 rewrite <- Heq; assumption
1032 end. 1032 end.
1033 rewrite pf.
1034 rewrite (lookup_type_inner wf pf).
1035 crush.
1036 repeat match goal with
1037 | [ H : _ = _ |- _ ] => rewrite (UIP_refl _ _ H) in *
1038 end.
1039 rewrite <- H.
1040 assumption.
1041 Qed. 1033 Qed.
1042 1034
1043 1035
1044 (** * Parametric version *) 1036 (** * Parametric version *)
1045 1037