blob: c9ce5f94bb50562d7ebed3b75ffd7e530b14037b (
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
|
Require Import Coq.Numbers.BinNums.
Local Generalizable All Variables.
Class pointed (T : Type) := point : T.
Global Hint Extern 5 (pointed _) => solve [ constructor ] : typeclass_instances.
Ltac step_pointed _ :=
(constructor + (unshelve (econstructor; revgoals); revgoals));
match goal with |- ?T => change (pointed T) end.
Ltac solve_pointed _ :=
step_pointed ();
exact _.
Local Hint Extern 6 (pointed _) => step_pointed () : typeclass_instances.
Local Hint Extern 7 (pointed _) => solve_pointed () : typeclass_instances.
Global Instance pointed_True : pointed True := _.
Global Instance pointed_unit : pointed unit := _.
Global Instance pointed_bool : pointed bool := _.
Global Instance pointed_list {A} : pointed (list A) := _.
Global Instance pointed_nat : pointed nat := _.
Global Instance pointed_N : pointed N := _.
Global Instance pointed_positive : pointed positive := _.
Global Instance pointed_Z : pointed Z := _.
Global Instance pointed_inhabited `{pointed A} : pointed (inhabited A) := _.
Global Instance pointed_sum_l {A B} {_ : pointed A} : pointed (A + B) | 2 := _.
Global Instance pointed_sum_r {A B} {_ : pointed B} : pointed (A + B) | 2 := _.
Global Instance pointed_or_l {A B : Prop} {_ : pointed A} : pointed (A \/ B) | 2 := _.
Global Instance pointed_or_r {A B : Prop} {_ : pointed B} : pointed (A \/ B) | 2 := _.
Global Instance pointed_prod `{pointed A, pointed B} : pointed (A * B) := _.
Global Instance pointed_and {A B : Prop} `{pointed A, pointed B} : pointed (A /\ B) := _.
Global Instance pointed_sig {A} {B : A -> Prop} {a : pointed A} {b : pointed (B a)} : pointed (sig B) := _.
Global Instance pointed_sigT {A B} {a : pointed A} {b : pointed (B a)} : pointed (sigT B) := _.
Global Instance pointed_sig2 {A} {B C : A -> Prop} {a : pointed A} {b : pointed (B a)} {c : pointed (C a)} : pointed (sig2 B C) := _.
Global Instance pointed_sigT2 {A B C} {a : pointed A} {b : pointed (B a)} {c : pointed (C a)} : pointed (sigT2 B C) := _.
Global Instance pointed_ex {A} {B : A -> Prop} {a : pointed A} {b : pointed (B a)} : pointed (ex B) := _.
Global Instance pointed_ex2 {A} {B C : A -> Prop} {a : pointed A} {b : pointed (B a)} {c : pointed (C a)} : pointed (ex2 B C) := _.
Global Instance pointed_ex_inhab {A} {B : A -> Prop} {a : pointed (inhabited A)} {b : forall a, pointed (B a)} : pointed (ex B)
:= match a return ex B with
| inhabits a => ex_intro _ a (b a)
end.
Global Instance pointed_ex2_inhab {A} {B C : A -> Prop} {a : pointed (inhabited A)} {b : forall a, pointed (B a)} {c : forall a, pointed (C a)} : pointed (ex2 B C)
:= match a return ex2 B C with
| inhabits a => ex_intro2 _ _ a (b a) (c a)
end.
Global Instance pointed_eq_refl {A x} : pointed (x = x :> A) := _.
Global Instance pointed_impl {A} {B : A -> Type} {f : forall a : pointed A, pointed (B a)} : pointed (forall a, B a) | 3 := f.
Global Instance pointed_Prop : pointed Prop := True.
Global Instance pointed_Set : pointed Set := True.
Global Instance pointed_Type : pointed Type := True.
|
