Add pointed types

For filling in default values

1 files changed, 54 insertions, 0 deletions

diff --git a/src/Util/Pointed.v b/src/Util/Pointed.v
new file mode 100644
index 000000000..c9ce5f94b
--- /dev/null
+++ b/src/Util/Pointed.v
@@ -0,0 +1,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.