Split out Reflection.Equality, change Tflat implicit argument

6 files changed, 99 insertions, 85 deletions

diff --git a/src/Reflection/Equality.v b/src/Reflection/Equality.v
new file mode 100644
index 000000000..39d2675b5
--- /dev/null
+++ b/src/Reflection/Equality.v
@@ -0,0 +1,92 @@
+Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Util.Decidable.
+
+Section language.
+  Context (base_type_code : Type)
+          (eq_base_type_code : base_type_code -> base_type_code -> bool)
+          (base_type_code_bl : forall x y, eq_base_type_code x y = true -> x = y)
+          (base_type_code_lb : forall x y, x = y -> eq_base_type_code x y = true).
+
+  Local Notation flat_type := (flat_type base_type_code).
+  Local Notation type := (type base_type_code).
+
+  Fixpoint flat_type_beq (X Y : flat_type) {struct X} : bool
+    := match X, Y with
+       | Tbase T, Tbase T0 => eq_base_type_code T T0
+       | Prod A B, Prod A0 B0 => (flat_type_beq A A0 && flat_type_beq B B0)%bool
+       | Tbase _, _
+       | Prod _ _, _
+         => false
+       end.
+  Local Ltac t :=
+    repeat match goal with
+           | _ => intro
+           | _ => reflexivity
+           | _ => assumption
+           | _ => progress simpl in *
+           | _ => solve [ eauto with nocore ]
+           | [ H : False |- _ ] => exfalso; assumption
+           | [ H : false = true |- _ ] => apply Bool.diff_false_true in H
+           | [ |- Prod _ _ = Prod _ _ ] => apply f_equal2
+           | [ |- Arrow _ _ = Arrow _ _ ] => apply f_equal2
+           | [ |- Tbase _ = Tbase _ ] => apply f_equal
+           | [ |- Tflat _ = Tflat _ ] => apply f_equal
+           | [ H : forall Y, _ = true -> _ = Y |- _ = ?Y' ]
+             => is_var Y'; apply H; solve [ t ]
+           | [ H : forall X Y, X = Y -> _ = true |- _ = true ]
+             => eapply H; solve [ t ]
+           | [ H : true = true |- _ ] => clear H
+           | [ H : andb ?x ?y = true |- _ ]
+             => destruct x, y; simpl in H; solve [ t ]
+           | [ H : andb ?x ?y = true |- _ ]
+             => destruct x eqn:?; simpl in H
+           | [ H : ?f ?x = true |- _ ] => destruct (f x); solve [ t ]
+           | [ H : ?x = true |- andb _ ?x = true ]
+             => destruct x
+           | [ |- andb ?x true = true ]
+             => cut (x = true); [ destruct x; simpl | ]
+           end.
+  Lemma flat_type_dec_bl X : forall Y, flat_type_beq X Y = true -> X = Y.
+  Proof. clear base_type_code_lb; induction X, Y; t. Defined.
+  Lemma flat_type_dec_lb X : forall Y, X = Y -> flat_type_beq X Y = true.
+  Proof. clear base_type_code_bl; intros; subst Y; induction X; t. Defined.
+  Definition flat_type_eq_dec (X Y : flat_type) : {X = Y} + {X <> Y}
+    := match Sumbool.sumbool_of_bool (flat_type_beq X Y) with
+       | left pf => left (flat_type_dec_bl _ _ pf)
+       | right pf => right (fun pf' => let pf'' := eq_sym (flat_type_dec_lb _ _ pf') in
+                                       Bool.diff_true_false (eq_trans pf'' pf))
+       end.
+  Fixpoint type_beq (X Y : type) {struct X} : bool
+    := match X, Y with
+       | Tflat T, Tflat T0 => flat_type_beq T T0
+       | Arrow A B, Arrow A0 B0 => (eq_base_type_code A A0 && type_beq B B0)%bool
+       | Tflat _, _
+       | Arrow _ _, _
+         => false
+       end.
+  Lemma type_dec_bl X : forall Y, type_beq X Y = true -> X = Y.
+  Proof. clear base_type_code_lb; pose proof flat_type_dec_bl; induction X, Y; t. Defined.
+  Lemma type_dec_lb X : forall Y, X = Y -> type_beq X Y = true.
+  Proof. clear base_type_code_bl; pose proof flat_type_dec_lb; intros; subst Y; induction X; t. Defined.
+  Definition type_eq_dec (X Y : type) : {X = Y} + {X <> Y}
+    := match Sumbool.sumbool_of_bool (type_beq X Y) with
+       | left pf => left (type_dec_bl _ _ pf)
+       | right pf => right (fun pf' => let pf'' := eq_sym (type_dec_lb _ _ pf') in
+                                       Bool.diff_true_false (eq_trans pf'' pf))
+       end.
+End language.
+
+Lemma dec_eq_flat_type {base_type_code} `{DecidableRel (@eq base_type_code)}
+  : DecidableRel (@eq (flat_type base_type_code)).
+Proof.
+  repeat intro; hnf; decide equality; apply dec; auto.
+Defined.
+Hint Extern 1 (Decidable (@eq (flat_type ?base_type_code) ?x ?y))
+=> simple apply (@dec_eq_flat_type base_type_code) : typeclass_instances.
+Lemma dec_eq_type {base_type_code} `{DecidableRel (@eq base_type_code)}
+  : DecidableRel (@eq (type base_type_code)).
+Proof.
+  repeat intro; hnf; decide equality; apply dec; typeclasses eauto.
+Defined.
+Hint Extern 1 (Decidable (@eq (type ?base_type_code) ?x ?y))
+=> simple apply (@dec_eq_type base_type_code) : typeclass_instances.
diff --git a/src/Reflection/MapCastWithCastOp.v b/src/Reflection/MapCastWithCastOp.v
index f896e71fb..189399fad 100644
--- a/src/Reflection/MapCastWithCastOp.v
+++ b/src/Reflection/MapCastWithCastOp.v
@@ -1,4 +1,5 @@
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Equality.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Reflection.MapCast.
 Require Import Crypto.Util.Sigma.
diff --git a/src/Reflection/MultiSizeTest2.v b/src/Reflection/MultiSizeTest2.v
index a0c9fc864..8dbc8f4ce 100644
--- a/src/Reflection/MultiSizeTest2.v
+++ b/src/Reflection/MultiSizeTest2.v
@@ -1,5 +1,6 @@
 Require Import Coq.omega.Omega.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Equality.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Reflection.MapCastWithCastOp.
 Require Import Crypto.Reflection.MapInterp.
diff --git a/src/Reflection/Syntax.v b/src/Reflection/Syntax.v
index 3f1fec3c7..f8d7cdcf3 100644
--- a/src/Reflection/Syntax.v
+++ b/src/Reflection/Syntax.v
@@ -1,7 +1,6 @@
 (** * PHOAS Representation of Gallina *)
 Require Import Coq.Strings.String Coq.Classes.RelationClasses Coq.Classes.Morphisms.
 Require Import Crypto.Util.Tuple.
-Require Import Crypto.Util.Decidable.
 Require Import Crypto.Util.LetIn.
 Require Import Crypto.Util.Tactics.
 Require Import Crypto.Util.Notations.
@@ -23,77 +22,6 @@ Section language.
   Inductive type := Tflat (T : flat_type) | Arrow (A : base_type_code) (B : type).
   Bind Scope ctype_scope with type.
 
-  Section dec.
-    Context (eq_base_type_code : base_type_code -> base_type_code -> bool)
-            (base_type_code_bl : forall x y, eq_base_type_code x y = true -> x = y)
-            (base_type_code_lb : forall x y, x = y -> eq_base_type_code x y = true).
-
-    Fixpoint flat_type_beq (X Y : flat_type) {struct X} : bool
-      := match X, Y with
-         | Tbase T, Tbase T0 => eq_base_type_code T T0
-         | Prod A B, Prod A0 B0 => (flat_type_beq A A0 && flat_type_beq B B0)%bool
-         | Tbase _, _
-         | Prod _ _, _
-           => false
-         end.
-    Local Ltac t :=
-      repeat match goal with
-             | _ => intro
-             | _ => reflexivity
-             | _ => assumption
-             | _ => progress simpl in *
-             | _ => solve [ eauto with nocore ]
-             | [ H : False |- _ ] => exfalso; assumption
-             | [ H : false = true |- _ ] => apply Bool.diff_false_true in H
-             | [ |- Prod _ _ = Prod _ _ ] => apply f_equal2
-             | [ |- Arrow _ _ = Arrow _ _ ] => apply f_equal2
-             | [ |- Tbase _ = Tbase _ ] => apply f_equal
-             | [ |- Tflat _ = Tflat _ ] => apply f_equal
-             | [ H : forall Y, _ = true -> _ = Y |- _ = ?Y' ]
-               => is_var Y'; apply H; solve [ t ]
-             | [ H : forall X Y, X = Y -> _ = true |- _ = true ]
-               => eapply H; solve [ t ]
-             | [ H : true = true |- _ ] => clear H
-             | [ H : andb ?x ?y = true |- _ ]
-               => destruct x, y; simpl in H; solve [ t ]
-             | [ H : andb ?x ?y = true |- _ ]
-               => destruct x eqn:?; simpl in H
-             | [ H : ?f ?x = true |- _ ] => destruct (f x); solve [ t ]
-             | [ H : ?x = true |- andb _ ?x = true ]
-               => destruct x
-             | [ |- andb ?x true = true ]
-               => cut (x = true); [ destruct x; simpl | ]
-             end.
-    Lemma flat_type_dec_bl X : forall Y, flat_type_beq X Y = true -> X = Y.
-    Proof. clear base_type_code_lb; induction X, Y; t. Defined.
-    Lemma flat_type_dec_lb X : forall Y, X = Y -> flat_type_beq X Y = true.
-    Proof. clear base_type_code_bl; intros; subst Y; induction X; t. Defined.
-    Definition flat_type_eq_dec (X Y : flat_type) : {X = Y} + {X <> Y}
-      := match Sumbool.sumbool_of_bool (flat_type_beq X Y) with
-         | left pf => left (flat_type_dec_bl _ _ pf)
-         | right pf => right (fun pf' => let pf'' := eq_sym (flat_type_dec_lb _ _ pf') in
-                                         Bool.diff_true_false (eq_trans pf'' pf))
-         end.
-    Fixpoint type_beq (X Y : type) {struct X} : bool
-      := match X, Y with
-         | Tflat T, Tflat T0 => flat_type_beq T T0
-         | Arrow A B, Arrow A0 B0 => (eq_base_type_code A A0 && type_beq B B0)%bool
-         | Tflat _, _
-         | Arrow _ _, _
-           => false
-         end.
-    Lemma type_dec_bl X : forall Y, type_beq X Y = true -> X = Y.
-    Proof. clear base_type_code_lb; pose proof flat_type_dec_bl; induction X, Y; t. Defined.
-    Lemma type_dec_lb X : forall Y, X = Y -> type_beq X Y = true.
-    Proof. clear base_type_code_bl; pose proof flat_type_dec_lb; intros; subst Y; induction X; t. Defined.
-    Definition type_eq_dec (X Y : type) : {X = Y} + {X <> Y}
-      := match Sumbool.sumbool_of_bool (type_beq X Y) with
-         | left pf => left (type_dec_bl _ _ pf)
-         | right pf => right (fun pf' => let pf'' := eq_sym (type_dec_lb _ _ pf') in
-                                         Bool.diff_true_false (eq_trans pf'' pf))
-         end.
-  End dec.
-
   Global Coercion Tflat : flat_type >-> type.
   Infix "*" := Prod : ctype_scope.
   Notation "A -> B" := (Arrow A B) : ctype_scope.
@@ -504,20 +432,10 @@ Global Arguments tuple {_}%type_scope _%ctype_scope _%nat_scope.
 Global Arguments Prod {_}%type_scope (_ _)%ctype_scope.
 Global Arguments Arrow {_}%type_scope (_ _)%ctype_scope.
 Global Arguments Tbase {_}%type_scope _%ctype_scope.
+Global Arguments Tflat {_}%type_scope _%ctype_scope.
 
 Ltac admit_Wf := apply Wf_admitted.
 
-Global Instance dec_eq_flat_type {base_type_code} `{DecidableRel (@eq base_type_code)}
-  : DecidableRel (@eq (flat_type base_type_code)).
-Proof.
-  repeat intro; hnf; decide equality; apply dec; auto.
-Defined.
-Global Instance dec_eq_type {base_type_code} `{DecidableRel (@eq base_type_code)}
-  : DecidableRel (@eq (type base_type_code)).
-Proof.
-  repeat intro; hnf; decide equality; apply dec; typeclasses eauto.
-Defined.
-
 Global Arguments Const {_ _ _ _ _} _.
 Global Arguments Var {_ _ _ _ _} _.
 Global Arguments SmartVarf {_ _ _ _ _} _.
diff --git a/src/Reflection/TestCase.v b/src/Reflection/TestCase.v
index a7e2146a6..640db3824 100644
--- a/src/Reflection/TestCase.v
+++ b/src/Reflection/TestCase.v
@@ -4,6 +4,7 @@ Require Import Crypto.Reflection.Named.Syntax.
 Require Import Crypto.Reflection.Named.Compile.
 Require Import Crypto.Reflection.Named.RegisterAssign.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Equality.
 Require Export Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.InputSyntax.
 Require Import Crypto.Reflection.CommonSubexpressionElimination.
@@ -81,7 +82,7 @@ Goal True.
   vm_compute in e.
 Abort.
 
-Definition example_expr : Syntax.Expr base_type interp_base_type op (Arrow Tnat (Arrow Tnat (Tflat _ tnat))).
+Definition example_expr : Syntax.Expr base_type interp_base_type op (Arrow Tnat (Arrow Tnat (Tflat tnat))).
 Proof.
   let x := Reify (fun z w => let unused := 1 + 1 in let x := 1 in let y := 1 in (let a := 1 in let '(c, d) := (2, 3) in a + x + (x + x) + (x + x) - (x + x) - a + c + d) + y + z + w)%nat in
   exact x.
@@ -202,7 +203,7 @@ Module bounds.
        | Prod _ _ => fun x => (constant_bounds _ (fst x), constant_bounds _ (snd x))
        end.
 
-  Definition example_expr_bounds : Syntax.Expr base_type interp_base_type_bounds op (Arrow Tnat (Arrow Tnat (Tflat _ tnat))) :=
+  Definition example_expr_bounds : Syntax.Expr base_type interp_base_type_bounds op (Arrow Tnat (Arrow Tnat (Tflat tnat))) :=
     Eval vm_compute in
       (fun var => map base_type op interp_base_type interp_base_type_bounds constant_bounds (fun _ x => x) (fun _ x => x) (example_expr (fun t => var t))).
 
diff --git a/src/Reflection/Z/Syntax.v b/src/Reflection/Z/Syntax.v
index 466dbd4b5..ea867d024 100644
--- a/src/Reflection/Z/Syntax.v
+++ b/src/Reflection/Z/Syntax.v
@@ -1,6 +1,7 @@
 (** * PHOAS Syntax for expression trees on ℤ *)
 Require Import Coq.ZArith.ZArith.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Equality.
 Require Import Crypto.ModularArithmetic.ModularBaseSystemListZOperations.
 Require Import Crypto.Util.Equality.
 Require Import Crypto.Util.ZUtil.