From 604a2659df73acadaaf3e879d25ba3b0ea09a151 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Wed, 11 Oct 2017 13:40:49 +0200
Subject: [PATCH] A bit of cleanup

---
 FiniteSets/HitTactics.v | 86 +++++++++++++++++++++++++++++++++++++++++
 FiniteSets/README.md    | 12 ++++++
 FiniteSets/_CoqProject  |  2 +-
 3 files changed, 99 insertions(+), 1 deletion(-)
 create mode 100644 FiniteSets/HitTactics.v
 create mode 100644 FiniteSets/README.md

diff --git a/FiniteSets/HitTactics.v b/FiniteSets/HitTactics.v
new file mode 100644
index 0000000..e71773c
--- /dev/null
+++ b/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.
+
diff --git a/FiniteSets/README.md b/FiniteSets/README.md
new file mode 100644
index 0000000..2889222
--- /dev/null
+++ b/FiniteSets/README.md
@@ -0,0 +1,12 @@
+# 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`
+
+An overview of some of the main results can be found in the file `CPP.v`
diff --git a/FiniteSets/_CoqProject b/FiniteSets/_CoqProject
index 1c8a3bc..1b6fd62 100644
--- a/FiniteSets/_CoqProject
+++ b/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