Finish CompileInterp proof

3 files changed, 120 insertions, 38 deletions

diff --git a/src/Reflection/Named/CompileInterp.v b/src/Reflection/Named/CompileInterp.v
index 3f8cb1562..6cb075f08 100644
--- a/src/Reflection/Named/CompileInterp.v
+++ b/src/Reflection/Named/CompileInterp.v
@@ -1,16 +1,21 @@
 (** * PHOAS → Named Representation of Gallina *)
 Require Import Crypto.Reflection.Named.Syntax.
 Require Import Crypto.Reflection.Named.NameUtil.
+Require Import Crypto.Reflection.Named.NameUtilProperties.
 Require Import Crypto.Reflection.Named.ContextDefinitions.
 Require Import Crypto.Reflection.Named.ContextProperties.
+Require Import Crypto.Reflection.Named.ContextProperties.NameUtil.
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.Wf.
 Require Import Crypto.Reflection.Named.Compile.
 Require Import Crypto.Util.PointedProp.
 Require Import Crypto.Util.Option.
 Require Import Crypto.Util.Decidable.
+Require Import Crypto.Util.Prod.
+Require Import Crypto.Util.ListUtil.
 Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.Tactics.DestructHead.
+Require Import Crypto.Util.Tactics.SpecializeBy.
 
 Local Open Scope ctype_scope.
 Local Open Scope nexpr_scope.
@@ -45,6 +50,8 @@ Section language.
         (HG : forall t n x, List.In (existT _ t (n, x)%core) G -> lookupb ctx n t = Some x)
         v
         (H : ocompilef e ls = Some v)
+        (Hls : oname_list_unique ls)
+        (HGls : forall t n x, List.In (existT _ t (n, x)%core) G -> List.In (Some n) ls -> False)
     : Named.interpf (interp_op:=interp_op) (ctx:=ctx) v
       = Some (interpf interp_op e').
   Proof.
@@ -60,7 +67,16 @@ Section language.
                    | progress break_innermost_match_step
                    | progress break_match_hyps
                    | progress destruct_head' or
+                   | progress inversion_prod
+                   | progress specialize_by_assumption
+                   | progress specialize_by auto using oname_list_unique_nil
                    | match goal with
+                     | [ H : forall x, oname_list_unique ?ls -> _ |- _ ]
+                       => specialize (fun pf x => H x pf)
+                     | [ H : context[snd (split_onames _ _)] |- _ ]
+                       => rewrite snd_split_onames_skipn in H
+                     | [ H : oname_list_unique (List.skipn _ _) -> _ |- _ ]
+                       => specialize (fun pf => H (@oname_list_unique_skipn _ _ _ pf))
                      | [ IH : forall v ls, ocompilef ?e ls = Some v -> _, H : ocompilef ?e ?ls' = Some ?v' |- _ ]
                        => specialize (IH _ _ H)
                      | [ IH : forall x1 x2 v ls, ocompilef (?e x1) ls = Some v -> _, H : ocompilef (?e ?x1') ?ls' = Some ?v' |- _ ]
@@ -71,8 +87,10 @@ Section language.
                        => rewrite H in H' by assumption
                      | [ H : forall x2 ctx, _ -> Named.interpf ?e = Some _ |- Named.interpf ?e = Some _ ]
                        => apply H; clear H
-                     end ].
-    { repeat match goal with
+                     | [ H : forall x2, _ -> forall ctx, _ -> Named.interpf ?e = Some _ |- Named.interpf ?e = Some _ ]
+                       => apply H; clear H
+                     end ];
+      repeat match goal with
              | _ => erewrite lookupb_extend by assumption
              | [ |- context[find_Name_and_val ?tdec ?ndec ?a ?b ?c ?d ?default] ]
                => lazymatch default with None => fail | _ => idtac end;
@@ -81,40 +99,98 @@ Section language.
              | _ => progress unfold dec in *
              | _ => progress break_innermost_match_step
              | _ => progress subst
+             | _ => progress destruct_head' and
              | _ => congruence
+             | [ H : List.In _ (flatten_binding_list _ _) |- _ ]
+               => erewrite <- (flatten_binding_list_find_Name_and_val_unique _ _) in H;
+                    [ | | apply path_prod_uncurried; split; [ eassumption | simpl; reflexivity ] ];
+                    [ | solve [ eauto using oname_list_unique_firstn, oname_list_unique_skipn ] ]
+             | [ H : _ |- _ ]
+               => first [ erewrite find_Name_and_val_wrong_type in H by eassumption
+                        | rewrite find_Name_and_val_different in H by assumption
+                        | rewrite snd_split_onames_skipn in H ]
+             | _ => solve [ eauto using In_skipn, In_firstn
+                          | eapply split_onames_find_Name_Some_unique; [ | apply path_prod; simpl | ]; eauto ]
+             | [ H : find_Name_and_val _ _ ?t ?n ?N ?V None = Some _, H' : List.In (Some ?n) (List.skipn _ ?ls) |- False ]
+               => eapply find_Name_and_val_find_Name_Some, split_onames_find_Name_Some_unique in H;
+                    [ | | apply path_prod_uncurried; split; [ eassumption | simpl; reflexivity ] ];
+                    [ | solve [ eauto using oname_list_unique_firstn, oname_list_unique_skipn ] ]
+             | [ H : List.In (existT _ ?t (?n, _)%core) ?G,
+                     H' : List.In (Some ?n) (List.skipn _ ?ls),
+                          IH : forall t' n' x', List.In (existT _ t' (n', x')%core) ?G -> List.In (Some n') ?ls -> False
+                                                |- False ]
+               => apply (IH _ _ _ H); clear IH H
+             | [ H : List.In (existT _ ?t (?n, _)%core) ?G,
+                     H' : find_Name _ ?n ?N = Some ?t',
+                          IH : forall t' n' x', List.In (existT _ t' (n', x')%core) ?G -> List.In (Some n') ?ls -> False
+                                                |- _ ]
+               => exfalso; apply (IH _ _ _ H); clear IH H
              end.
-      Focus 2.
-  Admitted.
-  (*
-  Fixpoint ocompilef {t} (e : exprf t) (ls : list (option Name)) {struct e}
-    : option (nexprf t)
-    := match e in @Syntax.exprf _ _ _ t return option (nexprf t) with
-       | TT => Some Named.TT
-       | Var _ x => Some (Named.Var x)
-       | Op _ _ op args => option_map (Named.Op op) (@ocompilef _ args ls)
-       | LetIn tx ex _ eC
-         => match @ocompilef _ ex nil, split_onames tx ls with
-            | Some x, (Some n, ls')%core
-              => option_map (fun C => Named.LetIn tx n x C) (@ocompilef _ (eC n) ls')
-            | _, _ => None
-            end
-       | Pair _ ex _ ey => match @ocompilef _ ex nil, @ocompilef _ ey nil with
-                           | Some x, Some y => Some (Named.Pair x y)
-                           | _, _ => None
-                           end
-       end.
+  Qed.
+
+  Lemma interp_ocompile (ctx : Context) {t} (e : expr t) e' (ls : list (option Name))
+        (Hwf : wf e e')
+        f
+        (Hls : oname_list_unique ls)
+        (H : ocompile e ls = Some f)
+    : forall v, Named.interp (interp_op:=interp_op) (ctx:=ctx) f v
+                = Some (interp interp_op e' v).
+  Proof.
+    revert H; destruct Hwf;
+      repeat first [ progress simpl in *
+                   | progress unfold option_map, Named.interp in *
+                   | congruence
+                   | progress break_innermost_match
+                   | progress inversion_option
+                   | progress subst
+                   | progress intros ].
+    eapply interpf_ocompilef;
+      [ eauto | | eassumption
+        | inversion_prod; subst; rewrite snd_split_onames_skipn; eauto using oname_list_unique_skipn
+        |intros ???; erewrite <- (flatten_binding_list_find_Name_and_val_unique _ _) by eassumption;
+         let H := fresh in
+         intro H; apply find_Name_and_val_find_Name_Some in H;
+         eapply split_onames_find_Name_Some_unique in H; [ | eassumption.. ];
+         intuition ].
+    { intros ???.
+      repeat first [ solve [ auto ]
+                   | rewrite (lookupb_extend Context _ _ _)
+                   | progress subst
+                   | progress break_innermost_match
+                   | erewrite <- (flatten_binding_list_find_Name_and_val_unique _ _) by eassumption
+                   | congruence
+                   | match goal with
+                     | [ |- context[find_Name_and_val ?tdec ?ndec ?a ?b ?c ?d ?default] ]
+                       => lazymatch default with None => fail | _ => idtac end;
+                          rewrite (find_Name_and_val_split tdec ndec (default:=default))
+                     | [ H : _ |- _ ] => first [ erewrite find_Name_and_val_wrong_type in H by eassumption
+                                               | erewrite find_Name_and_val_different in H by eassumption ]
+                     end
+                   | progress intros ]. }
+  Qed.
 
-  Definition ocompile {t} (e : expr t) (ls : list (option Name))
-    : option (nexpr t)
-    := match e in @Syntax.expr _ _ _ t return option (nexpr t) with
-       | Abs src _ f
-         => match split_onames src ls with
-            | (Some n, ls')%core
-              => option_map (Named.Abs n) (@ocompilef _ (f n) ls')
-            | _ => None
-            end
-       end.
+  Lemma interpf_compilef (ctx : Context) {t} (e : exprf t) e' (ls : list Name)
+        G
+        (Hwf : wff G e e')
+        (HG : forall t n x, List.In (existT _ t (n, x)%core) G -> lookupb ctx n t = Some x)
+        v
+        (H : compilef e ls = Some v)
+        (Hls : name_list_unique ls)
+        (HGls : forall t n x, List.In (existT _ t (n, x)%core) G -> List.In n ls -> False)
+    : Named.interpf (interp_op:=interp_op) (ctx:=ctx) v
+      = Some (interpf interp_op e').
+  Proof.
+    eapply interpf_ocompilef; try eassumption.
+    setoid_rewrite List.in_map_iff; intros; destruct_head' ex; destruct_head' and; inversion_option; subst.
+    eauto.
+  Qed.
 
-  Definition compilef {t} (e : exprf t) (ls : list Name) := @ocompilef t e (List.map (@Some _) ls).
-  Definition compile {t} (e : expr t) (ls : list Name) := @ocompile t e (List.map (@Some _) ls).*)
+  Lemma interp_compile (ctx : Context) {t} (e : expr t) e' (ls : list Name)
+        (Hwf : wf e e')
+        f
+        (Hls : name_list_unique ls)
+        (H : compile e ls = Some f)
+    : forall v, Named.interp (interp_op:=interp_op) (ctx:=ctx) f v
+                = Some (interp interp_op e' v).
+  Proof. eapply interp_ocompile; eassumption. Qed.
 End language.
diff --git a/src/Reflection/Named/NameUtil.v b/src/Reflection/Named/NameUtil.v
index 078449375..5356cd132 100644
--- a/src/Reflection/Named/NameUtil.v
+++ b/src/Reflection/Named/NameUtil.v
@@ -45,7 +45,7 @@ Section language.
   Definition oname_list_unique (ls : list (option Name)) : Prop
     := mname_list_unique (option Name) (fun x => x) ls.
   Definition name_list_unique (ls : list Name) : Prop
-    := mname_list_unique Name (@Some _) ls.
+    := oname_list_unique (List.map (@Some Name) ls).
 End language.
 
 Global Arguments split_mnames {_ _ MName} force _ _, {_ _} MName force _ _.
diff --git a/src/Reflection/Named/NameUtilProperties.v b/src/Reflection/Named/NameUtilProperties.v
index 4fe5d923a..7e5d28d31 100644
--- a/src/Reflection/Named/NameUtilProperties.v
+++ b/src/Reflection/Named/NameUtilProperties.v
@@ -141,10 +141,16 @@ Section language.
 
   Lemma name_list_unique_firstn n (ls : list Name)
     : name_list_unique ls -> name_list_unique (firstn n ls).
-  Proof. apply mname_list_unique_firstn. Qed.
+  Proof.
+    unfold name_list_unique; intro H; apply oname_list_unique_firstn with (n:=n) in H.
+    rewrite <- firstn_map; assumption.
+  Qed.
   Lemma name_list_unique_skipn n (ls : list Name)
     : name_list_unique ls -> name_list_unique (skipn n ls).
-  Proof. apply mname_list_unique_skipn. Qed.
+  Proof.
+    unfold name_list_unique; intro H; apply oname_list_unique_skipn with (n:=n) in H.
+    rewrite <- skipn_map; assumption.
+  Qed.
   Lemma name_list_unique_specialize (ls : list Name)
     : name_list_unique ls
       -> forall k n,
@@ -153,7 +159,7 @@ Section language.
         -> False.
   Proof.
     intros H k n; specialize (H k n).
-    rewrite firstn_map, skipn_map in H.
+    rewrite !map_id, !firstn_map, !skipn_map in H.
     eauto using in_map.
   Qed.
   Definition name_list_unique_nil : name_list_unique nil