Add base.{base_,}interp_beq

These are the canonical boolean equality functions for the interpretations of the various base types.  This will probably come in handy for side conditions in proofs about reifications of rewrite rules.

2 files changed, 54 insertions, 0 deletions

diff --git a/src/Language.v b/src/Language.v
index 044d19a3e..b3f3ddf1e 100644
--- a/src/Language.v
+++ b/src/Language.v
@@ -315,6 +315,23 @@ Module Compilers.
          | type.option A => Datatypes.option (interp A)
          end%type.
 
+    Fixpoint base_interp_beq {t} : base_interp t -> base_interp t -> bool
+      := match t with
+         | type.unit => fun _ _ => true
+         | type.Z => Z.eqb
+         | type.bool => Bool.eqb
+         | type.nat => Nat.eqb
+         | type.zrange => zrange_beq
+         end.
+
+    Fixpoint interp_beq {t} : interp t -> interp t -> bool
+      := match t with
+         | type.type_base t => @base_interp_beq t
+         | type.prod A B => prod_beq _ _ (@interp_beq A) (@interp_beq B)
+         | type.list A => list_beq _ (@interp_beq A)
+         | type.option A => option_beq (@interp_beq A)
+         end.
+
     Definition try_make_base_transport_cps
                (P : type.base -> Type) (t1 t2 : type.base)
       : ~> option (P t1 -> P t2)
diff --git a/src/LanguageInversion.v b/src/LanguageInversion.v
index 30d7fb3b4..5310ab3b0 100644
--- a/src/LanguageInversion.v
+++ b/src/LanguageInversion.v
@@ -92,6 +92,43 @@ Module Compilers.
       Ltac inversion_type := repeat inversion_type_step.
     End type.
 
+    Local Ltac beq_t :=
+      repeat first [ progress cbn in *
+                   | apply BinInt.Z.eqb_eq
+                   | apply Bool.eqb_true_iff
+                   | apply PeanoNat.Nat.eqb_eq
+                   | apply ZRange.zrange_bl
+                   | apply ZRange.zrange_lb
+                   | apply internal_prod_dec_bl
+                   | apply internal_prod_dec_lb
+                   | apply ListUtil.internal_list_dec_bl
+                   | apply ListUtil.internal_list_dec_lb
+                   | apply internal_option_dec_bl
+                   | apply internal_option_dec_lb
+                   | progress destruct_head'_unit
+                   | reflexivity
+                   | solve [ auto ] ].
+
+    Lemma base_interp_bl {t x y} : @base.base_interp_beq t x y = true -> x = y.
+    Proof. induction t; beq_t. Qed.
+    Local Hint Resolve base_interp_bl : core.
+
+    Lemma base_interp_lb {t x y} : x = y -> @base.base_interp_beq t x y = true.
+    Proof. induction t; beq_t. Qed.
+    Local Hint Resolve base_interp_lb : core.
+
+    Global Instance dec_eq_base_interp {t} : DecidableRel (@eq (@base.base_interp t)) | 10
+      := dec_rel_of_bool_dec_rel base.base_interp_beq (@base_interp_bl t) (@base_interp_lb t).
+
+    Lemma interp_bl {t x y} : @base.interp_beq t x y = true -> x = y.
+    Proof. induction t; beq_t. Qed.
+
+    Lemma interp_lb {t x y} : x = y -> @base.interp_beq t x y = true.
+    Proof. induction t; beq_t. Qed.
+
+    Global Instance dec_eq_interp {t} : DecidableRel (@eq (@base.interp t)) | 10
+      := dec_rel_of_bool_dec_rel base.interp_beq (@interp_bl t) (@interp_lb t).
+
     Global Instance Decidable_type_eq : DecidableRel (@eq base.type)
       := base.type.type_eq_dec.