Transparent versions of {flat_,}type_eq_dec

1 files changed, 71 insertions, 3 deletions

diff --git a/src/Reflection/Syntax.v b/src/Reflection/Syntax.v
index cc742d63d..98845ca27 100644
--- a/src/Reflection/Syntax.v
+++ b/src/Reflection/Syntax.v
@@ -23,6 +23,77 @@ 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.
@@ -429,9 +500,6 @@ Global Arguments Tbase {_}%type_scope _%ctype_scope.
 
 Ltac admit_Wf := apply Wf_admitted.
 
-Scheme Equality for flat_type.
-Scheme Equality for type.
-
 Global Instance dec_eq_flat_type {base_type_code} `{DecidableRel (@eq base_type_code)}
   : DecidableRel (@eq (flat_type base_type_code)).
 Proof.