Merge branch 'cleanupish'

FiniteSets/HitTactics.v

@@ -0,0 +1,86 @@
+Class HitRecursion (H : Type) := {
+  indTy : Type;
+  recTy : Type;
+  H_inductor : indTy;
+  H_recursor : recTy
+}.
+
+Definition hrecursion (H : Type) {HR : HitRecursion H} : @recTy H HR :=
+  @H_recursor H HR.
+
+Definition hinduction (H : Type) {HR : HitRecursion H} : @indTy H HR :=
+  @H_inductor H HR.
+
+
+(* TODO: use information from recTy instead of [typeof hrec]? *)
+Ltac hrecursion_ :=
+  lazymatch goal with
+  | [ |- ?T -> ?P ] => 
+    let hrec1 := eval cbv[hrecursion H_recursor] in (hrecursion T) in
+    let hrec := eval simpl in hrec1 in
+    let hrecTy1 := eval cbv[recTy] in (@recTy T _) in
+    let hrecTy := eval simpl in hrecTy1 in
+    match hrecTy with
+    | forall Y, T -> Y =>
+      simple refine (hrec P)
+    | forall Y _, T -> Y  =>
+      simple refine (hrec P _)
+    | forall Y _ _, T -> Y =>
+      simple refine (hrec P _ _)
+    | forall Y _ _ _, T -> Y  =>
+      simple refine (hrec P _ _ _)
+    | forall Y _ _ _ _, T -> Y  =>
+      simple refine (hrec P _ _ _ _)
+    | forall Y _ _ _ _ _, T -> Y =>
+      simple refine (hrec P _ _ _ _ _)
+    | forall Y _ _ _ _ _ _, T -> Y =>
+      simple refine (hrec P _ _ _ _ _ _)
+    | forall Y _ _ _ _ _ _ _, T -> Y =>
+      simple refine (hrec P _ _ _ _ _ _ _)
+    | forall Y _ _ _ _ _ _ _ _, T -> Y =>
+      simple refine (hrec P _ _ _ _ _ _ _ _)
+    | forall Y _ _ _ _ _ _ _ _ _, T -> Y => 
+      simple refine (hrec P _ _ _ _ _ _ _ _ _)
+    | forall Y _ _ _ _ _ _ _ _ _ _, T -> Y =>
+      simple refine (hrec P _ _ _ _ _ _ _ _ _ _) 
+    | _ => fail "Cannot handle the recursion principle (too many parameters?) :("
+    end
+  | [ |- forall (target:?T), ?P] => 
+    let hind1 := eval cbv[hinduction H_inductor] in (hinduction T) in
+    let hind := eval simpl in hind1 in
+    match type of hind with
+    | ?Q => 
+      match (eval simpl in Q) with
+      | forall Y , (forall x, Y x) =>
+        simple refine (hind (fun target => P) _)
+      | forall Y _, (forall x, Y x)  =>
+        simple refine (hind (fun target => P) _)
+      | forall Y _ _, (forall x, Y x)  =>
+        simple refine (hind (fun target => P) _ _)
+      | forall Y _ _ _, (forall x, Y x)  =>       
+        simple refine (hind (fun target => P) _ _ _)
+      | forall Y _ _ _ _, (forall x, Y x)  =>
+        simple refine (hind (fun target => P) _ _ _ _)
+      | forall Y _ _ _ _ _, (forall x, Y x)  =>
+        simple refine (hind (fun target => P) _ _ _ _ _)
+      | forall Y _ _ _ _ _ _, (forall x, Y x)  =>
+        simple refine (hind (fun target => P) _ _ _ _ _ _)
+      | forall Y _ _ _ _ _ _ _, (forall x, Y x)  =>
+        simple refine (hind (fun target => P) _ _ _ _ _ _ _)
+      | forall Y _ _ _ _ _ _ _, (forall x, Y x)  =>
+        simple refine (hind (fun target => P) _ _ _ _ _ _ _)
+      | forall Y _ _ _ _ _ _ _ _, (forall x, Y x)  =>
+        simple refine (hind (fun target => P) _ _ _ _ _ _ _ _)
+      | forall Y _ _ _ _ _ _ _ _ _, (forall x, Y x)  =>
+        simple refine (hind (fun target => P) _ _ _ _ _ _ _ _ _)
+      | _ => fail "Cannot handle the induction principle (too many parameters?) :("
+     end
+    end
+  (*| _ => fail "I am sorry, but something went wrong!"*)
+  end.
+
+Tactic Notation "hrecursion" := hrecursion_; simpl.
+Tactic Notation "hrecursion" ident(x) := revert x; hrecursion.
+Tactic Notation "hinduction" := hrecursion_; simpl.
+Tactic Notation "hinduction" ident(x) := revert x; hrecursion.
+

FiniteSets/README.md

@@ -0,0 +1,13 @@
+# Formalization of Kuratowski-finite sets in homotopy type theory
+
+The Coq docs can be found [here](http://cs.ru.nl/~dfrumin/haan/fsets/)
+
+# Building instructions
+
+Prerequisites: the [HoTT library](https://github.com/HoTT/HoTT).
+
+1. Generate the Makefile: `coq_makefile -f _CoqProject -o Makefile`
+2. Compile the library using make: `make -j 2`
+3. The HTML coqdoc can be obtained via `make html`
+
+An overview of some of the main results can be found in the file `CPP.v`

FiniteSets/_CoqProject

@@ -1,5 +1,5 @@
 -R . "" COQC = hoqc COQDEP = hoqdep
--R ../prelude ""
+HitTactics.v
 prelude.v
 interfaces/lattice_interface.v
 interfaces/lattice_examples.v