From a8c07fa7605eefa2de39000d4c6fce17fb40be43 Mon Sep 17 00:00:00 2001
From: Jason Gross <jagro@google.com>
Date: Thu, 2 Aug 2018 18:12:24 -0400
Subject: Add GENERATEDIdentifiersWithoutTypesProofs.v

---
 _CoqProject                                        |  1 +
 .../GENERATEDIdentifiersWithoutTypesProofs.v       | 71 ++++++++++++++++++++++
 2 files changed, 72 insertions(+)
 create mode 100644 src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypesProofs.v

diff --git a/_CoqProject b/_CoqProject
index fc49cbf15..30aab707b 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -249,6 +249,7 @@ src/Experiments/NewPipeline/CLI.v
 src/Experiments/NewPipeline/CStringification.v
 src/Experiments/NewPipeline/CompilersTestCases.v
 src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v
+src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypesProofs.v
 src/Experiments/NewPipeline/Language.v
 src/Experiments/NewPipeline/LanguageInversion.v
 src/Experiments/NewPipeline/LanguageWf.v
diff --git a/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypesProofs.v b/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypesProofs.v
new file mode 100644
index 000000000..d5374e8ce
--- /dev/null
+++ b/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypesProofs.v
@@ -0,0 +1,71 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Crypto.Util.CPSNotations.
+Require Import Crypto.Util.ZRange.
+Require Import Crypto.Util.Tactics.BreakMatch.
+Require Import Crypto.Util.Option.
+Require Import Crypto.Experiments.NewPipeline.Language.
+Require Import Crypto.Experiments.NewPipeline.GENERATEDIdentifiersWithoutTypes.
+
+Import EqNotations.
+Module Compilers.
+  Import Language.Compilers.
+  Import GENERATEDIdentifiersWithoutTypes.Compilers.
+
+  Module pattern.
+    Import GENERATEDIdentifiersWithoutTypes.Compilers.pattern.
+    Module ident.
+      Import GENERATEDIdentifiersWithoutTypes.Compilers.pattern.ident.
+
+      Local Lemma quick_invert_eq_option {A} (P : Type) (x y : option A) (H : x = y)
+        : match x, y return Type with
+          | Some _, None => P
+          | None, Some _ => P
+          | _, _ => True
+          end.
+      Proof. subst y; destruct x; constructor. Qed.
+
+      Lemma pident_to_typed_invert_bind_args_type__pident_to_typed_invert_bind_args t idc p f
+        : @invert_bind_args t idc p = Some f
+          -> { pf : t = type_of p f | @to_typed p f = rew [Compilers.ident.ident] pf in idc }.
+      Proof.
+        cbv [invert_bind_args type_of full_types].
+        repeat first [ reflexivity
+                     | (exists eq_refl)
+                     | progress intros
+                     | match goal with
+                       | [ H : Some _ = None |- ?P ] => exact (@quick_invert_eq_option _ P _ _ H)
+                       | [ H : None = Some _ |- ?P ] => exact (@quick_invert_eq_option _ P _ _ H)
+                       end
+                     | progress inversion_option
+                     | progress subst
+                     | break_innermost_match_step
+                     | break_innermost_match_hyps_step ].
+      Qed.
+
+      Lemma pident_to_typed_invert_bind_args_type t idc p f
+        : @invert_bind_args t idc p = Some f -> t = type_of p f.
+      Proof.
+        intro pf; exact (proj1_sig (@pident_to_typed_invert_bind_args_type__pident_to_typed_invert_bind_args t idc p f pf)).
+      Defined.
+
+      Lemma pident_to_typed_invert_bind_args t idc p f (pf : @invert_bind_args t idc p = Some f)
+        : @to_typed p f = rew [Compilers.ident.ident] @pident_to_typed_invert_bind_args_type t idc p f pf in idc.
+      Proof.
+        exact (proj2_sig (@pident_to_typed_invert_bind_args_type__pident_to_typed_invert_bind_args t idc p f pf)).
+      Defined.
+
+      Lemma try_make_transport_ident_cps_correct P idc1 idc2 T k
+        : try_make_transport_ident_cps P idc1 idc2 T k
+          = k (match Sumbool.sumbool_of_bool (ident_beq idc1 idc2) with
+               | left pf => Some (fun v => rew [P] internal_ident_dec_bl _ _ pf in v)
+               | right _ => None
+               end).
+      Proof.
+        destruct (Sumbool.sumbool_of_bool (ident_beq idc1 idc2)) as [pf|pf].
+        { generalize (internal_ident_dec_bl idc1 idc2 pf); clear pf; intro; subst idc2; cbn [eq_rect].
+          destruct idc1; reflexivity. }
+        { destruct idc1, idc2; try reflexivity; solve [ inversion pf ]. }
+      Qed.
+    End ident.
+  End pattern.
+End Compilers.
-- 
cgit v1.2.3