blob: cbe16b7ba61b1c327d550db54cb3f840167e16d0 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
|
(** * Well-foundedness of changing the interp function on PHOAS Representation of Gallina *)
Require Import Coq.Strings.String Coq.Classes.RelationClasses.
Require Import Crypto.Reflection.Syntax.
Require Import Crypto.Reflection.MapInterp.
Require Import Crypto.Reflection.WfRel.
Require Import Crypto.Util.Tuple.
Require Import Crypto.Util.Tactics.
Require Import Crypto.Util.Notations.
Local Open Scope ctype_scope.
Local Open Scope expr_scope.
Section language.
Context {base_type_code : Type}
{interp_base_type interp_base_type1 interp_base_type2 : base_type_code -> Type}
{op : flat_type base_type_code -> flat_type base_type_code -> Type}
(f1 : forall t, interp_base_type t -> interp_base_type1 t)
(f2 : forall t, interp_base_type t -> interp_base_type2 t)
(R : forall t, interp_base_type1 t -> interp_base_type2 t -> Prop)
(Rf12 : forall t v, R t (f1 t v) (f2 t v)).
Section with_var.
Context {var1 var2 : base_type_code -> Type}.
Lemma flat_rel_pointwise2_mapf {t} (v : interp_flat_type interp_base_type t)
: interp_flat_type_rel_pointwise2
R
(mapf_interp_flat_type f1 v)
(mapf_interp_flat_type f2 v).
Proof. induction t; simpl; auto. Qed.
Lemma wff_mapf_interp {t e1 e2} G
(Hwf : @wff base_type_code interp_base_type op var1 var2 G t e1 e2)
: wff G (mapf_interp f1 e1) (mapf_interp f1 e2).
Proof. induction Hwf; constructor; auto. Qed.
Lemma rel_wff_mapf_interp {t e1 e2} G
(Hwf : @wff base_type_code interp_base_type op var1 var2 G t e1 e2)
: rel_wff R G (mapf_interp f1 e1) (mapf_interp f2 e2).
Proof. induction Hwf; constructor; auto using flat_rel_pointwise2_mapf. Qed.
Lemma wf_map_interp {t e1 e2} G
(Hwf : @wf base_type_code interp_base_type op var1 var2 G t e1 e2)
: wf G (map_interp f1 e1) (map_interp f1 e2).
Proof. induction Hwf; constructor; auto using wff_mapf_interp. Qed.
Lemma rel_wf_map_interp {t e1 e2} G
(Hwf : @wf base_type_code interp_base_type op var1 var2 G t e1 e2)
: rel_wf R G (map_interp f1 e1) (map_interp f2 e2).
Proof. induction Hwf; constructor; auto using rel_wff_mapf_interp. Qed.
End with_var.
Lemma WfMapInterp {t e} (Hwf : @Wf base_type_code interp_base_type op t e)
: Wf (MapInterp f1 e).
Proof. repeat intro; apply wf_map_interp, Hwf. Qed.
Lemma RelWfMapInterp {t e} (Hwf : @Wf base_type_code interp_base_type op t e)
: RelWf R (MapInterp f1 e) (MapInterp f2 e).
Proof. repeat intro; apply rel_wf_map_interp, Hwf. Qed.
End language.
|
