From 240cbebf3b2c14e5c064ea81392714562c9fb79c Mon Sep 17 00:00:00 2001
From: gabrielhdt <gabrielhondet@gmail.com>
Date: Wed, 26 Feb 2020 15:00:04 +0100
Subject: [PATCH] prelude split by chapters
---
adlib/cert_f/induction.lp | 8 +++
prelude/cert_f/booleans.lp | 14 ----
prelude/cert_f/equalities.lp | 3 -
prelude/cert_f/equality_props.lp | 22 ------
prelude/cert_f/if_def.lp | 3 -
prelude/cert_f/logic.lp | 114 +++++++++++++++++++++++++++++++
prelude/cert_f/notequal.lp | 4 --
prelude/cert_f/xor_def.lp | 18 -----
8 files changed, 122 insertions(+), 64 deletions(-)
create mode 100644 adlib/cert_f/induction.lp
delete mode 100644 prelude/cert_f/booleans.lp
delete mode 100644 prelude/cert_f/equalities.lp
delete mode 100644 prelude/cert_f/equality_props.lp
delete mode 100644 prelude/cert_f/if_def.lp
create mode 100644 prelude/cert_f/logic.lp
delete mode 100644 prelude/cert_f/notequal.lp
delete mode 100644 prelude/cert_f/xor_def.lp
diff --git a/adlib/cert_f/induction.lp b/adlib/cert_f/induction.lp
new file mode 100644
index 0000000..38442e6
--- /dev/null
+++ b/adlib/cert_f/induction.lp
@@ -0,0 +1,8 @@
+require open encodings.cert_f
+prelude.cert_f.booleans
+
+// Allows to make case disjunction in proofs,
+// [refine disjunction P ?Cfalse ?Ctrue]
+// to create two new subgoals
+symbol disjunction (P: Term bool ⇒ Term bool):
+ Term (P false) ⇒ Term (P true) ⇒ ∀ x, Term (P x)
diff --git a/prelude/cert_f/booleans.lp b/prelude/cert_f/booleans.lp
deleted file mode 100644
index d01c31f..0000000
--- a/prelude/cert_f/booleans.lp
+++ /dev/null
@@ -1,14 +0,0 @@
-require open encodings.cert_f
-
-definition bool ≔ uProp
-definition false ≔ @prod Type Prop uProp (λ x, x)
-definition true ≔ @prod Prop Prop false (λ _, false)
-
-definition imp (P Q: Term uProp) ≔ @prod Prop Prop P (λ_, Q)
-
-definition bnot (P: Term uProp) ≔ @prod Prop Prop P (λ _, false)
-set prefix 5 "¬" ≔ bnot
-definition band (P Q: Term uProp) ≔ bnot (imp P (bnot Q))
-set infix 6 "∧" ≔ band
-definition bor (P Q: Term uProp) ≔ imp (bnot P) Q
-set infix 5 "∨" ≔ bor
diff --git a/prelude/cert_f/equalities.lp b/prelude/cert_f/equalities.lp
deleted file mode 100644
index 83456f6..0000000
--- a/prelude/cert_f/equalities.lp
+++ /dev/null
@@ -1,3 +0,0 @@
-require open encodings.cert_f prelude.cert_f.booleans
-
-symbol eq {T: Term uType}: Term T ⇒ Term T ⇒ Term uProp
diff --git a/prelude/cert_f/equality_props.lp b/prelude/cert_f/equality_props.lp
deleted file mode 100644
index 33ba4c8..0000000
--- a/prelude/cert_f/equality_props.lp
+++ /dev/null
@@ -1,22 +0,0 @@
-require open encodings.cert_f
-prelude.cert_f.booleans
-prelude.cert_f.equalities
-prelude.cert_f.if_def
-
-rule if true &t _ → &t
- and if false _ &f → &f
-
-theorem if_same T (b: Term uProp) (x: Term T):
- Term (eq (if b x x) x)
-proof
-assume T b x
-simpl
-admit // Needs case disjunciton on boolean
-
-symbol reflexivity_of_equal T (x: Term T) : Term (eq x x)
-
-symbol transitivity_of_equal T (x y z: Term T) :
- Term ((eq x y) ∧ (eq y z)) ⇒ Term (eq x z)
-
-symbol symmetry_of_equal T (x y: Term T):
- Term (eq x y) ⇒ Term (eq y x)
diff --git a/prelude/cert_f/if_def.lp b/prelude/cert_f/if_def.lp
deleted file mode 100644
index 37aaea9..0000000
--- a/prelude/cert_f/if_def.lp
+++ /dev/null
@@ -1,3 +0,0 @@
-require open encodings.cert_f prelude.cert_f.booleans
-
-symbol if {T: Term uType} : Term uProp ⇒ Term T ⇒ Term T ⇒ Term T
diff --git a/prelude/cert_f/logic.lp b/prelude/cert_f/logic.lp
new file mode 100644
index 0000000..bb2f192
--- /dev/null
+++ b/prelude/cert_f/logic.lp
@@ -0,0 +1,114 @@
+require open encodings.cert_f
+require adlib.cert_f.induction as I
+
+//
+// Booleans
+//
+definition bool ≔ uProp
+definition false: Term bool ≔ @prod Type Prop uProp (λ x, x)
+definition true: Term bool ≔ @prod Prop Prop false (λ _, false)
+
+definition imp (P Q: Term uProp) ≔ @prod Prop Prop P (λ_, Q)
+definition forall {eT: Term uType} (P: Term eT ⇒ Term bool) ≔
+ @prod _ _ eT P
+// FIXME explicitness?
+
+definition bnot (P: Term uProp) ≔ @prod Prop Prop P (λ _, false)
+set prefix 5 "¬" ≔ bnot
+definition band (P Q: Term uProp) ≔ bnot (imp P (bnot Q))
+set infix 6 "∧" ≔ band
+definition bor (P Q: Term uProp) ≔ imp (bnot P) Q
+set infix 5 "∨" ≔ bor
+
+definition biff (P Q: Term uProp) ≔ (imp P Q) ∧ (imp Q P)
+set infix 7 "⇔" ≔ biff
+
+definition when (P Q: Term uProp) ≔ imp Q P
+
+//
+// Equalities
+//
+symbol eq {T: Term uType}: Term T ⇒ Term T ⇒ Term uProp
+
+//
+// Notequal
+//
+definition neq {T: Term uType} (x y: Term T) ≔ bnot (eq x y)
+set infix left 6 "/=" ≔ neq
+set declared "≠"
+set infix left 6 "≠" ≔ neq
+
+//
+// if_def
+//
+symbol if {T: Term uType} : Term uProp ⇒ Term T ⇒ Term T ⇒ Term T
+// The reduction rules for if are in [equality_props]
+
+//
+// boolean_props
+// Slightly modified from the prelude
+constant symbol bool_exclusive: Term (@neq bool false true)
+constant symbol bool_inclusive A: Term ((@eq bool A false) ∨ (@eq bool A true))
+
+theorem excluded_middle (A: Term bool): Term (A ∨ ¬ A)
+proof
+admit
+
+//
+// xor_def
+//
+// FIXME explicitness required
+definition xor (a b: Term bool) ≔ @neq bool a b
+
+set flag "print_implicits" on
+// FIXME explicitness required
+theorem xor_def: ∀ (a b: Term bool),
+ Term (@eq bool (xor a b) (@if bool a (bnot b) b))
+proof
+assume a
+refine I.disjunction
+ (λx: Term bool, @eq bool (xor a x) (@if bool a (bnot x) x))
+ ?Cf[a] ?Ct[a]
+// FIXME needs generalize?
+admit
+
+//
+// Quantifier props
+//
+set declared "∃"
+// Declared as a lemma in the prelude
+definition ∃ {eT: Term uType} (P: Term eT ⇒ Term bool) ≔
+ Term (¬ (forall (λx, ¬ (P x))))
+
+//
+// Defined types
+//
+
+//
+// exists1
+//
+
+//
+// equality_props
+//
+rule if true &t _ → &t
+ and if false _ &f → &f
+
+theorem if_same T (b: Term uProp) (x: Term T):
+ Term (eq (if b x x) x)
+proof
+assume T b x
+simpl
+admit // Needs case disjunciton on boolean
+
+symbol reflexivity_of_equal T (x: Term T) : Term (eq x x)
+
+symbol transitivity_of_equal T (x y z: Term T) :
+ Term ((eq x y) ∧ (eq y z)) ⇒ Term (eq x z)
+
+symbol symmetry_of_equal T (x y: Term T):
+ Term (eq x y) ⇒ Term (eq y x)
+
+//
+// if_props
+//
diff --git a/prelude/cert_f/notequal.lp b/prelude/cert_f/notequal.lp
deleted file mode 100644
index 8238a93..0000000
--- a/prelude/cert_f/notequal.lp
+++ /dev/null
@@ -1,4 +0,0 @@
-require open encodings.cert_f prelude.cert_f.booleans prelude.cert_f.equalities
-
-definition neq {T: Term uType} (x y: Term T) ≔ bnot (eq x y)
-set infix left 6 "/=" ≔ neq
diff --git a/prelude/cert_f/xor_def.lp b/prelude/cert_f/xor_def.lp
deleted file mode 100644
index f64cd2e..0000000
--- a/prelude/cert_f/xor_def.lp
+++ /dev/null
@@ -1,18 +0,0 @@
-require open encodings.cert_f prelude.cert_f.booleans prelude.cert_f.equalities
-prelude.cert_f.notequal prelude.cert_f.if_def
-
-// FIXME explicitness required
-definition xor (a b: Univ Prop) ≔ @neq uProp a b
-
-type ∀ (a b: Univ Prop), Term (xor a b)
-
-type λ (a: Term uProp), @if uProp a a a
-type ∀ a : Term uProp, Term (@if uProp a a a)
-
-// FIXME explicitness required
-theorem xor_def: ∀ (a b: Univ Prop),
- Term (@eq uProp (xor a b) (@if uProp a (bnot b) b))
-proof
-assume a b
-simpl
-admit
--
GitLab