More proofs about wf / interp

3 files changed, 52 insertions, 23 deletions

diff --git a/src/Experiments/NewPipeline/Language.v b/src/Experiments/NewPipeline/Language.v
index e68127690..afd028ee8 100644
--- a/src/Experiments/NewPipeline/Language.v
+++ b/src/Experiments/NewPipeline/Language.v
@@ -1435,12 +1435,6 @@ Module Compilers.
            end.
     End with_var.
 
-    Definition reify_list {var} {t : base.type} (ls : list (@expr.expr base.type ident var (type.base t))) : expr (type.base (base.type.list t))
-      := fold_right
-           (fun x xs => x :: xs)%expr
-           []%expr
-           ls.
-
     Fixpoint reflect_list_cps' {var t} (e : @expr.expr base.type ident var t) {struct e}
       : ~> option (list (@expr.expr base.type ident var (type.base match t return base.type with
                                                                    | type.base (base.type.list t) => t
@@ -1565,27 +1559,16 @@ Module Compilers.
 
   Module GallinaReify.
     Module base.
-      Fixpoint value (t : base.type) : Set
-        := match t with
-           | base.type.unit as t
-           | base.type.Z as t
-           | base.type.bool as t
-           | base.type.nat as t
-             => base.interp t
-           | base.type.prod A B => value A * value B
-           | base.type.list A => list (value A)
-           end%type.
-
       Section reify.
         Context {var : type -> Type}.
         Fixpoint reify {t : base.type} {struct t}
-          : value t -> @expr var t
-          := match t return value t -> expr t with
+          : base.interp t -> @expr var t
+          := match t return base.interp t -> expr t with
              | base.type.prod A B as t
-               => fun '((a, b) : value A * value B)
+               => fun '((a, b) : base.interp A * base.interp B)
                   => (@reify A a, @reify B b)%expr
              | base.type.list A as t
-               => fun x : list (value A)
+               => fun x : list (base.interp A)
                   => reify_list (List.map (@reify A) x)
              | base.type.unit as t
              | base.type.Z as t
@@ -1596,7 +1579,7 @@ Module Compilers.
              end.
       End reify.
 
-      Definition Reify_as (t : base.type) (v : value t) : Expr t
+      Definition Reify_as (t : base.type) (v : base.interp t) : Expr t
         := fun var => reify v.
 
       (** [Reify] does Ltac type inference to get the type *)
@@ -1609,7 +1592,7 @@ Module Compilers.
       Fixpoint value (t : type)
         := match t return Type with
            | type.arrow s d => var s -> value d
-           | type.base t => base.value t
+           | type.base t => base.interp t
            end%type.
     End value.
 
diff --git a/src/Experiments/NewPipeline/LanguageInversion.v b/src/Experiments/NewPipeline/LanguageInversion.v
index c0247a1e1..b0db97e75 100644
--- a/src/Experiments/NewPipeline/LanguageInversion.v
+++ b/src/Experiments/NewPipeline/LanguageInversion.v
@@ -594,6 +594,13 @@ Module Compilers.
       Qed.
       Lemma reflect_list_Some_nil {t} {e : expr (base.type.list t)} : invert_expr.reflect_list e = Some nil -> e = (#ident.nil)%expr.
       Proof. exact (@reflect_list_Some _ e nil). Qed.
+      Lemma reflect_reify_list {t} {v} : invert_expr.reflect_list (var:=var) (reify_list (t:=t) v) = Some v.
+      Proof.
+        induction v as [|v vs IHvs]; rewrite ?reify_list_cons, ?reify_list_nil, reflect_list_step; [ reflexivity | ].
+        cbn; cbv [option_map]; cbv [type_base] in *; rewrite IHvs; reflexivity.
+      Qed.
+      Lemma reflect_list_Some_iff  {t} {e : expr (base.type.list t)} {v} : invert_expr.reflect_list e = Some v <-> e = reify_list v.
+      Proof. split; intro; subst; apply reflect_reify_list || apply reflect_list_Some; assumption. Qed.
     End with_var2.
 
     Ltac invert_subst_step_helper guard_tac :=
diff --git a/src/Experiments/NewPipeline/LanguageWf.v b/src/Experiments/NewPipeline/LanguageWf.v
index c9d0877b6..c8b19a5f4 100644
--- a/src/Experiments/NewPipeline/LanguageWf.v
+++ b/src/Experiments/NewPipeline/LanguageWf.v
@@ -401,8 +401,47 @@ Module Compilers.
                             | progress inversion_wf_one_constr
                             | progress expr.invert_match ].
         Qed.
+
+        Lemma wf_reify {t} v G : expr.wf G (@GallinaReify.base.reify var1 t v) (@GallinaReify.base.reify var2 t v).
+        Proof.
+          induction t; cbn; break_innermost_match; repeat constructor; auto; [].
+          rewrite wf_reify_list, !map_length, combine_map_map, combine_same, map_map; split; auto; intros *; [].
+          cbn [fst snd]; rewrite in_map_iff; intros.
+          repeat first [ progress destruct_head'_and
+                       | progress destruct_head'_ex
+                       | progress inversion_prod
+                       | progress subst
+                       | solve [ eauto ] ].
+        Qed.
       End with_var2.
+
+      Lemma Wf_Reify_as {t} v : expr.Wf (@GallinaReify.base.Reify_as t v).
+      Proof. repeat intro; apply wf_reify. Qed.
+
+      Section interp.
+        Import defaults.
+        Lemma interp_reify_list {t} ls : interp (reify_list (t:=t) ls) = List.map interp ls.
+        Proof.
+          cbv [reify_list]; induction ls as [|l ls IHls]; [ reflexivity | ];
+            cbn [list_rect map expr.interp ident.interp ident.gen_interp]; rewrite <- IHls;
+              reflexivity.
+        Qed.
+
+        Lemma interp_reify {t} v : interp (GallinaReify.base.reify (t:=t) v) = v.
+        Proof.
+          induction t; cbn [GallinaReify.base.reify]; break_innermost_match; cbn; f_equal;
+            rewrite ?interp_reify_list, ?map_map; auto.
+          { etransitivity; [ | apply map_id ]; apply map_ext; auto. }
+        Qed.
+
+        Lemma Interp_Reify_as {t} v : Interp (GallinaReify.base.Reify_as t v) = v.
+        Proof. apply interp_reify. Qed.
+      End interp.
     End invert.
+
+    (** [Reify] is a notation for [Reify_as] + better type inference, so we make [Wf_Reify] available for ease of memory / lookup *)
+    Notation Wf_Reify := Wf_Reify_as.
+    Notation Interp_Reify := Interp_Reify_as.
   End expr.
 
   Local Ltac destructure_step :=