diff options
author | Jason Gross <jgross@mit.edu> | 2017-02-28 18:32:43 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-02-28 18:32:43 -0500 |
commit | 80dc66a34fbf031bfac1214ccbb3bb1dcdef3d39 (patch) | |
tree | 8c68edebce0f80c507dc0a382936540a44bb94a3 /src | |
parent | 945bb1c6483d3cce338a4bc70e0a8a0c2551071c (diff) |
Add interp_flat_type_rel_pointwise_SmartVarfMap, interp_flat_type_rel_pointwise_Reflexive
Diffstat (limited to 'src')
-rw-r--r-- | src/Reflection/Relations.v | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/src/Reflection/Relations.v b/src/Reflection/Relations.v index 4a277d2b1..4109651c8 100644 --- a/src/Reflection/Relations.v +++ b/src/Reflection/Relations.v @@ -141,6 +141,23 @@ Section language. -> (interp_flat_type_rel_pointwise R1 t y x -> interp_flat_type_rel_pointwise R2 t x y). Proof. induction t; simpl; intuition. Qed. + + Global Instance interp_flat_type_rel_pointwise_Reflexive {R : forall t, _ -> _ -> Prop} {H : forall t, Reflexive (R t)} + : forall t, Reflexive (@interp_flat_type_rel_pointwise interp_base_type1 interp_base_type1 R t). + Proof. + induction t; intro; simpl; try apply conj; try reflexivity. + Qed. + + Lemma interp_flat_type_rel_pointwise_SmartVarfMap + {interp_base_type1' interp_base_type2'} + {R : forall t, _ -> _ -> Prop} + t f g x y + : @interp_flat_type_rel_pointwise interp_base_type1 interp_base_type2 R t (SmartVarfMap f x) (SmartVarfMap g y) + <-> @interp_flat_type_rel_pointwise interp_base_type1' interp_base_type2' (fun t x y => R t (f _ x) (g _ y)) t x y. + Proof. + induction t; simpl; try reflexivity. + rewrite_hyp <- !*; reflexivity. + Qed. End flat_type_extra. Section type. |