diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Language.v | 17 | ||||
| -rw-r--r-- | src/LanguageInversion.v | 37 |
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. |