# HG changeset patch # User Adam Chlipala # Date 1226935360 18000 # Node ID 71c076dd5f313e775b5cc3d0a970a7908336027a # Parent ecd231ba5c8b97bbe1512fc970527ccc6302a982 Close to automated ccExp_correct diff -r ecd231ba5c8b -r 71c076dd5f31 src/Intensional.v --- a/src/Intensional.v Sun Nov 16 19:58:01 2008 -0500 +++ b/src/Intensional.v Mon Nov 17 10:22:40 2008 -0500 @@ -232,6 +232,15 @@ Notation "f <== \\ x , y , e ; fs" := (Abs (fun x y => e) (fun f => fs)) (right associativity, at level 80, e at next level) : cc_scope. + Notation "f <== \\ ! , y , e ; fs" := + (Abs (fun _ y => e) (fun f => fs)) + (right associativity, at level 80, e at next level) : cc_scope. + Notation "f <== \\ x , ! , e ; fs" := + (Abs (fun x _ => e) (fun f => fs)) + (right associativity, at level 80, e at next level) : cc_scope. + Notation "f <== \\ ! , ! , e ; fs" := + (Abs (fun _ _ => e) (fun f => fs)) + (right associativity, at level 80, e at next level) : cc_scope. Notation "x <- e1 ; e2" := (Let e1 (fun x => e2)) (right associativity, at level 80, e1 at next level) : cc_scope. @@ -325,8 +334,6 @@ Import Source. Open Local Scope source_scope. - Hint Extern 3 False => omega. - Fixpoint lookup_type (envT : list Source.type) (n : nat) {struct envT} : isfree envT -> option Source.type := match envT return (isfree envT -> _) with @@ -505,13 +512,11 @@ Lemma lookup_bound_contra : forall t envT (fvs : isfree envT), lookup_type (length envT) fvs = Some t -> False. - intros; assert (length envT < length envT); eauto. + intros; assert (length envT < length envT); eauto; crush. Defined. Hint Resolve lookup_bound_contra. - Hint Extern 3 (_ = _) => elimtype False; omega. - Lemma lookup_push_drop : forall v t t' envT fvs, v < length envT -> lookup_type (envT := t :: envT) v (true, fvs) = Some t' @@ -625,17 +630,6 @@ Section lookup_hints. Hint Resolve lookup_bound_contra. - (*Ltac my_chooser T k := - match T with - | ptype => - match goal with - | [ H : lookup _ _ = Some ?t |- _ ] => k t - end - | _ => default_chooser T k - end. - - Ltac my_matching := matching equation my_chooser.*) - Hint Resolve lookup_bound_contra. Lemma lookup_type_push : forall t' envT (fvs1 fvs2 : isfree envT) b1 b2, @@ -761,11 +755,14 @@ Implicit Arguments env_prog [envT]. - Axiom cheat : forall T, T. - Import Source. Open Local Scope cc_scope. + Definition proj1 A B (pf : A /\ B) : A := + let (x, _) := pf in x. + Definition proj2 A B (pf : A /\ B) : B := + let (_, y) := pf in y. + Fixpoint ccExp var t (e : Source.exp natvar t) (envT : list Source.type) (fvs : isfree envT) {struct e} : wfExp fvs e -> env_prog var (ccType t) fvs := @@ -812,7 +809,41 @@ fun _ => map_funcs (fun f => f tt) (ccExp (E _) (envT := nil) tt Hwf). -(** * Correctness *) +(** ** Examples *) + +Open Local Scope source_scope. + +Definition ident : Source.Exp (Nat --> Nat) := fun _ => \x, #x. +Theorem ident_ok : wfExp (envT := nil) tt (ident _). + crush. +Defined. +Eval compute in CcExp' ident ident_ok. +Eval compute in ProgDenote (CcExp' ident ident_ok). + +Definition app_ident : Source.Exp Nat := fun _ => ident _ @ ^0. +Theorem app_ident_ok : wfExp (envT := nil) tt (app_ident _). + crush. +Defined. +Eval compute in CcExp' app_ident app_ident_ok. +Eval compute in ProgDenote (CcExp' app_ident app_ident_ok). + +Definition first : Source.Exp (Nat --> Nat --> Nat) := fun _ => + \x, \y, #x. +Theorem first_ok : wfExp (envT := nil) tt (first _). + crush. +Defined. +Eval compute in CcExp' first first_ok. +Eval compute in ProgDenote (CcExp' first first_ok). + +Definition app_first : Source.Exp Nat := fun _ => first _ @ ^1 @ ^0. +Theorem app_first_ok : wfExp (envT := nil) tt (app_first _). + crush. +Defined. +Eval compute in CcExp' app_first app_first_ok. +Eval compute in ProgDenote (CcExp' app_first app_first_ok). + + +(** ** Correctness *) Section spliceFuncs_correct. Variables T1 T2 : Type. @@ -914,9 +945,9 @@ apply False_rect; exact H end. - Theorem packExp_correct : forall v envT (fvs1 fvs2 : isfree envT) + Theorem packExp_correct : forall v t envT (fvs1 fvs2 : isfree envT) Hincl env, - lookup_type v fvs1 <> None + lookup_type v fvs1 = Some t -> lookup Closed.typeDenote v env == lookup Closed.typeDenote v (makeEnv (Closed.expDenote @@ -925,10 +956,9 @@ Qed. End packing_correct. -About packExp_correct. Implicit Arguments packExp_correct [v envT fvs1]. - -Implicit Arguments lookup_type_more [v2 envT fvs t b v]. +Implicit Arguments lookup_type_inner [t t' envT v t'' fvs e]. +Implicit Arguments inclusion [t t' envT fvs e]. Lemma typeDenote_same : forall t, Source.typeDenote t = Closed.typeDenote (ccType t). @@ -937,14 +967,6 @@ Hint Resolve typeDenote_same. -Lemma look : forall envT n (fvs : isfree envT) t, - lookup_type n fvs = Some t - -> Closed.typeDenote <| lookup_type n fvs = Source.typeDenote t. - crush. -Qed. - -Implicit Arguments look [envT n fvs t]. - Fixpoint lr (t : Source.type) : Source.typeDenote t -> Closed.typeDenote (ccType t) -> Prop := match t return Source.typeDenote t -> Closed.typeDenote (ccType t) -> Prop with | Nat => @eq nat @@ -968,75 +990,53 @@ lr t v1 (match lok pf in _ = T return T with | refl_equal => lookup Closed.typeDenote v2 env end)) - (*-> forall pf : lookup_type v2 fvs = Some t, - lr t v1 (match pf in _ = T return Closed.typeDenote <| T with - | refl_equal => lookup Closed.typeDenote v2 env - end))*) -> lr t (Source.expDenote e1) (Closed.expDenote (funcsDenote (ccExp e2 fvs wf) env)). Hint Rewrite spliceFuncs_correct unpackExp_correct : cpdt. Hint Resolve packExp_correct lookup_type_inner. - induction 1. + induction 1; crush. + + match goal with + | [ IH : _, Hlr : lr ?T ?X1 ?X2, ENV : list Source.type, F2 : natvar _ -> _ |- _ ] => + apply (IH X1 (length ENV) (T :: ENV) (true, snd (fvsExp (F2 (length ENV)) (T :: ENV)))) + end. crush. - crush. - crush. - crush. + match goal with + | [ Hlt : forall t v1 v2, _ -> _ < _, Hin : In _ _ |- _ ] => + generalize (Hlt _ _ _ Hin); crush + end. - crush. - apply (H0 x1 (length envT) (t1 :: envT) (true, snd (fvsExp (f2 (length envT)) (t1 :: envT)))). - clear H0. - crush. - eauto. - generalize (H1 _ _ _ H4). - crush. - - crush. - generalize H3; clear_all. + crush; match goal with | [ |- context[match ?pf with refl_equal => _ end] ] => generalize pf - end. - simpl. - destruct (eq_nat_dec (length envT) (length envT)); crush. - rewrite (UIP_refl _ _ e0); assumption. + end; simpl; + match goal with + | [ |- context[if ?E then _ else _] ] => destruct E + end; intuition; subst; + try match goal with + | [ |- context[match ?pf with refl_equal => _ end] ] => rewrite (UIP_refl _ _ pf); assumption + | [ Hlt : forall t v1 v2, _ -> _ < _, Hin : In (existT _ _ (_, length _)) _ |- _ ] => + generalize (Hlt _ _ _ Hin); crush + end. - match goal with - | [ |- context[match ?pf with refl_equal => _ end] ] => generalize pf - end; simpl. - destruct (eq_nat_dec v2 (length envT)); crush. - generalize (H1 _ _ _ H5). - crush. - generalize (H2 _ _ _ H5). - clear H2; intro H2. - generalize (H2 (lookup_type_inner _ _ _ _ _ wf pf)). - clear H2; intro H2. - generalize H2; clear_all. + generalize (H2 _ _ _ H5 (lookup_type_inner wf pf)); clear_all. repeat match goal with | [ |- context[match ?pf with refl_equal => _ end] ] => generalize pf end; simpl. - - match type of pf with - | ?X = _ => assert (X <> None) - end. - congruence. - assert (forall (n : nat) (t0 : Source.type), - lookup_type (envT:=envT) n (snd (fvsExp (f2 (length envT)) (t1 :: envT))) = Some t0 -> - lookup_type (envT:=envT) n fvs = Some t0). - eauto. - generalize (packExp_correct fvs (inclusion t1 envT fvs (f2 (length envT)) wf) env H). - simpl. + generalize (packExp_correct _ fvs (inclusion wf) env pf); simpl. match goal with | [ |- ?X == ?Y -> _ ] => generalize X Y end. rewrite pf. - rewrite (lookup_type_inner _ _ _ _ _ wf pf). + rewrite (lookup_type_inner wf pf). crush. - rewrite (UIP_refl _ _ e0). - rewrite (UIP_refl _ _ e1) in H2. - crush. - rewrite <- H1. + repeat match goal with + | [ H : _ = _ |- _ ] => rewrite (UIP_refl _ _ H) in * + end. + rewrite <- H. assumption. Qed.