blob: c1405cf91fef8e6a67d2e9cbeec4a954c6c73365 (
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
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
139
140
141
142
143
144
|
Section group_morphism.
(* An example with default canonical structures *)
Variable A B : Type.
Variable plusA : A -> A -> A.
Variable plusB : B -> B -> B.
Variable zeroA : A.
Variable zeroB : B.
Variable eqA : A -> A -> Prop.
Variable eqB : B -> B -> Prop.
Variable phi : A -> B.
Record img := {
ia : A;
ib :> B;
prf : phi ia = ib
}.
Parameter eq_img : forall (i1:img) (i2:img),
eqB (ib i1) (ib i2) -> eqA (ia i1) (ia i2).
Lemma phi_img (a:A) : img.
intro a.
exists a (phi a).
refine ( refl_equal _).
Defined.
Canonical Structure phi_img.
Lemma zero_img : img.
exists zeroA zeroB.
admit.
Defined.
Canonical Structure zero_img.
Lemma plus_img : img -> img -> img.
intros i1 i2.
exists (plusA (ia i1) (ia i2)) (plusB (ib i1) (ib i2)).
admit.
Defined.
Canonical Structure plus_img.
(* Print Canonical Projections. *)
Goal forall a1 a2, eqA (plusA a1 zeroA) a2.
intros a1 a2.
refine (eq_img _ _ _).
change (eqB (plusB (phi a1) zeroB) (phi a2)).
Admitted.
End group_morphism.
Open Scope type_scope.
Section type_reification.
Inductive term :Type :=
Fun : term -> term -> term
| Prod : term -> term -> term
| Bool : term
| SET :term
| PROP :term
| TYPE :term
| Var : Type -> term.
Fixpoint interp (t:term) :=
match t with
Bool => bool
| SET => Set
| PROP => Prop
| TYPE => Type
| Fun a b => interp a -> interp b
| Prod a b => interp a * interp b
| Var x => x
end.
Record interp_pair :Type :=
{ repr:>term;
abs:>Type;
link: abs = interp repr }.
Lemma prod_interp :forall (a b:interp_pair),a * b = interp (Prod a b) .
proof.
let a:interp_pair,b:interp_pair.
reconsider thesis as (a * b = interp a * interp b).
thus thesis by (link a),(link b).
end proof.
Qed.
Lemma fun_interp :forall (a b:interp_pair), (a -> b) = interp (Fun a b).
proof.
let a:interp_pair,b:interp_pair.
reconsider thesis as ((a -> b) = (interp a -> interp b)).
thus thesis using rewrite (link a);rewrite (link b);reflexivity.
end proof.
Qed.
Canonical Structure ProdCan (a b:interp_pair) :=
Build_interp_pair (Prod a b) (a * b) (prod_interp a b).
Canonical Structure FunCan (a b:interp_pair) :=
Build_interp_pair (Fun a b) (a -> b) (fun_interp a b).
Canonical Structure BoolCan :=
Build_interp_pair Bool bool (refl_equal _).
Canonical Structure VarCan (x:Type) :=
Build_interp_pair (Var x) x (refl_equal _).
Canonical Structure SetCan :=
Build_interp_pair SET Set (refl_equal _).
Canonical Structure PropCan :=
Build_interp_pair PROP Prop (refl_equal _).
Canonical Structure TypeCan :=
Build_interp_pair TYPE Type (refl_equal _).
(* Print Canonical Projections. *)
Variable A:Type.
Variable Inhabited: term -> Prop.
Variable Inhabited_correct: forall p, Inhabited (repr p) -> abs p.
Lemma L : Prop * A -> bool * (Type -> Set) .
refine (Inhabited_correct _ _).
change (Inhabited (Fun (Prod PROP (Var A)) (Prod Bool (Fun TYPE SET)))).
Admitted.
Check L : abs _ .
End type_reification.
|
