-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathex_ulcbeta.v
154 lines (109 loc) · 2.68 KB
/
ex_ulcbeta.v
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
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
Require Export CatSem.PROP_untyped.prop_arities_initial.
Require Import Coq.Program.Equality.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Automatic Introduction.
Unset Transparent Obligations.
(* Check INITIAL_INEQ_REP. *)
Inductive Lambda_index := ABS | APP.
Definition Lambda : Signature := {|
sig_index := Lambda_index ;
sig := fun x => match x with
| ABS => [[ 1 ]]
| APP => [[ 0 ; 0]]
end
|}.
(*Definition Lambda_subst := subst_half_eq Lambda.
Check Lambda_subst.
*)
Section App_Abs_half_eq.
Section for_a_representation.
Variable R : REP Lambda.
Definition beta_carrier :
(forall c : TYPE, (S_Mod_classic_ob [[1; 0]] R) c ---> (S_Mod_classic_ob [[0]] R) c) .
simpl.
intros.
simpl in *.
inversion X.
simpl in *.
inversion X1.
simpl in X2.
constructor.
simpl.
destruct R as [Rr Repr].
simpl in *.
apply (Repr APP).
simpl.
simpl in *.
constructor.
simpl.
apply (Repr ABS).
simpl.
constructor.
simpl.
apply X0.
constructor.
constructor.
simpl.
apply X2.
constructor.
constructor.
Defined.
Program Instance beta_struct : RModule_Hom_struct
(M:=S_Mod_classic_ob [[1;0]] R) (N:=S_Mod_classic_ob [[0]] R) beta_carrier.
Next Obligation.
Proof.
dependent destruction x.
simpl.
dependent destruction x.
simpl in *.
apply CONSTR_eq; auto.
destruct R.
simpl in *.
rerew (rmhom_rmkl (repr APP)).
apply f_equal.
simpl in *.
apply CONSTR_eq; auto.
clear x.
clear p0.
rerew (rmhom_rmkl (repr ABS)).
Qed.
Definition beta_module_mor := Build_RModule_Hom beta_struct.
End for_a_representation.
Program Instance beta_half_s : half_equation_struct
(U:=S_Mod_classic Lambda [[1 ; 0]])
(V:=S_Mod_classic Lambda [[0]])
beta_module_mor.
Next Obligation.
Proof.
dependent destruction x.
dependent destruction x.
dependent destruction x.
simpl.
apply CONSTR_eq; auto.
destruct T; simpl.
destruct R; simpl.
assert (H:=@repr_hom_s _ _ _ _ f).
simpl in *.
assert (Habs := H ABS).
simpl in *.
unfold commute in Habs; simpl in *.
assert (Happ := H APP).
simpl in *.
unfold commute in Happ; simpl in *.
rewrite <- Happ.
apply f_equal.
simpl in *.
apply CONSTR_eq; auto.
rewrite <- Habs.
auto.
Qed.
Definition beta_half_eq := Build_half_equation beta_half_s.
End App_Abs_half_eq.
Definition beta_rule : ineq_classic Lambda := {|
half_eq_l := beta_half_eq ;
half_eq_r := subst_half_eq Lambda |}.
Definition Lambda_beta_Cat := INEQ_REP
(S:=Lambda)(A:=unit)(fun x : unit => beta_rule).
Definition Lambda_beta_SynSem := (INITIAL_INEQ_REP (fun x : unit => beta_rule)).
Definition Lambda_beta := @Init _ _ _ (INITIAL_INEQ_REP (fun x : unit => beta_rule)).