forked from JasonGross/slow-coq-examples
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathslow_typeclasses_intro.v
118 lines (94 loc) · 4.1 KB
/
slow_typeclasses_intro.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
(* Lifted from https://coq.inria.fr/bugs/show_bug.cgi?id=3448 *)
Axiom proof_admitted : False.
Tactic Notation "admit" := abstract case proof_admitted.
Require Program.Tactics.
Generalizable All Variables.
Class ILogicOps Frm := {
lentails: Frm -> Frm -> Prop;
lforall: forall {T}, (T -> Frm) -> Frm;
lexists: forall {T}, (T -> Frm) -> Frm
}.
Infix "|--" := lentails (at level 79, no associativity).
Notation "'Forall' x .. y , p" :=
(lforall (fun x => .. (lforall (fun y => p)) .. )) (at level 78, x binder, y binder, right associativity).
Notation "'Exists' x .. y , p" :=
(lexists (fun x => .. (lexists (fun y => p)) .. )) (at level 78, x binder, y binder, right associativity).
Section ILogic_Pre.
Context (T : Type) .
Context `{ILOps: ILogicOps Frm}.
Record ILPreFrm := mkILPreFrm {
ILPreFrm_pred :> T -> Frm;
ILPreFrm_closed: forall t t': T,
ILPreFrm_pred t |-- ILPreFrm_pred t'
}.
Notation "'mk'" := @mkILPreFrm.
Program Definition ILPre_Ops : ILogicOps ILPreFrm := {|
lentails P Q := forall t:T, P t |-- Q t;
lforall A P := mk (fun t => Forall a, P a t) _;
lexists A P := mk (fun t => Exists a, P a t) _
|}.
Admit Obligations.
End ILogic_Pre.
Implicit Arguments ILPreFrm [T [ILOps]].
Implicit Arguments mkILPreFrm [T Frm ILOps].
Section ILogic_Fun.
Context (T: Type).
Context `{ILOps: ILogicOps Frm}.
Definition ILFunFrm := T -> Frm .
Program Definition ILFun_Ops : ILogicOps ILFunFrm := {|
lentails P Q := forall t:T, P t |-- Q t;
lforall A P := (fun t => Forall a, P a t);
lexists A P := (fun t => Exists a, P a t)
|}.
End ILogic_Fun.
Set Implicit Arguments.
Axiom PState : Type.
Definition SPred := @ILFunFrm PState Prop.
Axiom sepSP : SPred -> SPred -> SPred.
Axiom eq_pred : PState -> SPred.
Local Existing Instance ILFun_Ops.
Local Existing Instance ILPre_Ops.
Instance ILogicOps_Prop : ILogicOps Prop | 2 := {
lentails := fun (P : Prop) (Q : Prop) => P -> Q;
lforall T F := forall x:T, F x;
lexists T F := exists x:T, F x
}.
Definition spec := @ILPreFrm nat (@ILPreFrm SPred Prop _) _.
Definition mkspec (f: nat -> SPred -> Prop)
(HSPred: forall k P P', f k P -> f k P') : spec.
Proof.
refine (mkILPreFrm (fun k => mkILPreFrm (f k) _) _).
repeat intro.
simpl in *.
admit.
Grab Existential Variables.
admit.
Defined.
Definition spec_fun (S: spec) := fun k P => S k P.
Coercion spec_fun: spec >-> Funclass.
Definition spec_at (S: spec) (R: SPred) : spec.
Proof.
refine (mkspec (fun k P => S k (sepSP R P)) _); admit.
Defined.
Infix "@" := spec_at (at level 44, left associativity).
Class AtEx S := at_ex: forall A f, Forall x:A, S @ f x |-- S @ lexists f.
Module slow.
Axiom AtEx_at : forall S R {HS: AtEx S}, AtEx (S @ R).
Local Hint Extern 1 (AtEx _) => apply AtEx_at : typeclass_instances.
Typeclasses eauto := debug.
Goal forall S R (HS : AtEx S) a, eq_pred a |-- R -> AtEx (S @ eq_pred a).
Proof.
Time typeclasses eauto. (* 0.247 s *)
Undo.
Time intros; typeclasses eauto. (* 0 s *)
Admitted.
End slow.
Module fast.
Axiom AtEx_at : forall S R {HS: AtEx S}, AtEx (S @ R).
Local Hint Extern 1 AtEx => apply AtEx_at : typeclass_instances.
Typeclasses eauto := debug.
Goal forall S R (HS : AtEx S) a, eq_pred a |-- R -> AtEx (S @ eq_pred a).
Proof.
Time typeclasses eauto. (* 0.004 s *)
Defined.
End fast.