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
|
Require Import ssreflect ssrfun ssrbool.
From elpi Require Import elpi.
From HB Require Import structures.
#[verbose] HB.mixin Record hasA T := { a : T }.
About hasA.type.
HB.structure Definition A := {T of hasA T}.
HB.mixin Record hasB T := { b : T * T }.
About hasB.type.
HB.structure Definition B := {T of hasB T}.
#[short(pack="AB.pack")]
HB.structure Definition AB := {T of hasA T & hasB T}.
HB.factory Record hasAB T := { a : T; b : T * T }.
HB.builders Context T of hasAB T.
Definition xxx := HB.pack_for AB.type T (hasB.Build T b) (hasA.Build T a).
HB.instance Definition _ := AB.copy T xxx.
HB.end.
About hasAB.type.
HB.factory Definition hasA' T := hasA T.
About hasA'.type.
Section test.
Variables (G : Prop) (P : AB.type -> G).
(* problem with planB
Goal forall T (a b : T), G.
Proof.
move=> T a b.
pose Ta := hasA.Build _ a.
pose A := ltac:(elpi HB.pack_for (A.type) (T) (Ta)).
pose Tab := hasB.Build A (b,b).
pose AB : AB.type := ltac:(elpi HB.pack (A) (Tab)).
exact: P AB.
Qed.
*)
Goal forall T (a b : T), G.
Proof.
move=> T a b.
pose Ta := hasA.Build _ a.
pose A := HB.pack_for A.type T Ta.
pose Tab := hasB.Build A (b,b).
pose AB := HB.pack_for AB.type A Tab.
exact: P AB.
Qed.
Goal forall T (a b : T), G.
Proof.
move=> T a b.
pose Ta := hasA.Build _ a.
pose A : A.type := HB.pack T Ta.
pose Tab := hasB.Build A (b,b).
pose AB : AB.type := HB.pack A Tab.
exact: P AB.
Qed.
Check forall T : AB.type,
let x := AB.pack T in
x.
Goal forall T (a b : T), G.
Proof.
move=> T a b.
unshelve epose (A := HB.pack_for A.type T (_ : hasA T)).
by exact: (hasA.Build _ a).
Check A : A.type.
unshelve epose (A1 := HB.pack_for A.type T (hasA.Build T _)).
by exact: a.
Check A : A.type.
pose AB1 := AB.pack A (_ : hasB _).
Check AB1 : hasB A -> AB.type.
have [:Bm] @AB2 := AB.pack A (Bm : hasB A).
by exact: (hasB.Build _ (b,b)).
Check Bm : hasB A.
Check AB2 : AB.type.
have [:pB] @AB3 := AB.pack A (hasB.Build A pB).
by exact: (b,b).
Check pB : T * T.
Check AB3 : AB.type.
have [:pA pB'] @AB4 := AB.pack T (hasAB.Build A pA pB').
by exact: a.
by exact: (b,b).
exact: P AB4.
Qed.
End test.
HB.mixin Record HasFoo (A : Type) (P : A -> Prop) T := {
foo : forall x, P x -> T;
}.
#[short(pack="Foo.pack")]
HB.structure Definition Foo A P := { T of HasFoo A P T }.
Section test2.
Variable A : Type.
Variable P : A -> Prop.
Goal forall T, (forall x, P x -> T) -> True.
intros T H.
pose X := Foo.pack T (HasFoo.Build A P T H).
Check X : Foo.type A P.
Abort.
End test2.
HB.mixin Record isID T (F : T -> T) := { p : forall x : T, F x = x }.
HB.structure Definition Fun T := { F of isID T F }.
Goal forall f : nat -> nat, forall p : (forall x, f x = x ), True.
intros f p.
pose F := isID.Build nat f p.
pose T : Fun.type nat := HB.pack f F.
Check T : Fun.type nat.
Abort.
|
