From 616e9974e80d2494167c29ce47243a2947f92a8a Mon Sep 17 00:00:00 2001
From: gabrielhdt <gabrielhondet@gmail.com>
Date: Mon, 24 Feb 2020 11:12:28 +0100
Subject: [PATCH] more
---
adlib/cert_f/nat.lp | 27 +++++++++++++++++++++++----
encodings/cert_f.lp | 2 +-
prelude/cert_f/booleans.lp | 7 +++++++
prelude/cert_f/equality_props.lp | 22 ++++++++++++++++++++++
prelude/cert_f/if_def.lp | 3 ---
sandbox/cert_f/even.lp | 25 +++++++++++++++++++++++++
sandbox/cert_f/rat.lp | 27 ++++++++++++++++++++++-----
7 files changed, 100 insertions(+), 13 deletions(-)
create mode 100644 prelude/cert_f/equality_props.lp
create mode 100644 sandbox/cert_f/even.lp
diff --git a/adlib/cert_f/nat.lp b/adlib/cert_f/nat.lp
index 57a4dc6..29f08e2 100644
--- a/adlib/cert_f/nat.lp
+++ b/adlib/cert_f/nat.lp
@@ -2,15 +2,34 @@ require open encodings.cert_f prelude.cert_f.booleans
prelude.cert_f.equalities prelude.cert_f.notequal
prelude.cert_f.naturalnumbers
-definition not_zero ≔ neq 0
-definition nznat ≔ psub nat not_zero
-
symbol times : Term nat ⇒ Term nat ⇒ Term nat
+symbol plus : Term nat ⇒ Term nat ⇒ Term nat
+set infix left 6 "+" ≔ plus
+set infix left 7 "*" ≔ times
+
+rule (succ &n) + &m → succ (&n + &m)
+ and 0 + &m → &m
+ and &n + (succ &m) → succ (&n + &m)
+ and &n + 0 → &n
+
+rule (succ &n) * &m → &n * &m + &m
+ and 0 * _ → 0
+ and &n * (succ &m) → &n * &m + &n
+ and _ * 0 → 0
+
+symbol prod_comm (x y: Term nat): Term (eq (times x y) (times y x))
+
+
+//
+// Non zero naturals
+//
+definition not_zero ≔ neq 0
+type not_zero
symbol prod_not_zero (x y: Term nat):
Term (not_zero x) ⇒ Term (not_zero y) ⇒ Term (not_zero (times x y))
-symbol prod_comm (x y: Term nat): Term (eq (times x y) (times y x))
+definition nznat ≔ psub nat not_zero
// Constructor of nznat
definition nznatc (x: Term nat) (h: Term (not_zero x)) : Term nznat ≔
diff --git a/encodings/cert_f.lp b/encodings/cert_f.lp
index 328af9d..72f5053 100644
--- a/encodings/cert_f.lp
+++ b/encodings/cert_f.lp
@@ -27,7 +27,7 @@ injective symbol Term {s : Sort} : Univ s ⇒ TYPE
rule Term uProp → Univ Prop
and Term uType → Univ Type
-// [prod s1 s2 A B] encodes [Î x : (A: s1). (B x: s2)]
+// [prod s1 s2 A B] encodes [Î x : (A: s1). (B: s2)]
symbol prod {s1 s2 : Sort} (A : Univ s1) :
(Term A ⇒ Univ s2) ⇒ Univ (Rule s1 s2)
diff --git a/prelude/cert_f/booleans.lp b/prelude/cert_f/booleans.lp
index 4a01fef..d01c31f 100644
--- a/prelude/cert_f/booleans.lp
+++ b/prelude/cert_f/booleans.lp
@@ -4,4 +4,11 @@ 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/equality_props.lp b/prelude/cert_f/equality_props.lp
new file mode 100644
index 0000000..33ba4c8
--- /dev/null
+++ b/prelude/cert_f/equality_props.lp
@@ -0,0 +1,22 @@
+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
index a4276a8..37aaea9 100644
--- a/prelude/cert_f/if_def.lp
+++ b/prelude/cert_f/if_def.lp
@@ -1,6 +1,3 @@
require open encodings.cert_f prelude.cert_f.booleans
symbol if {T: Term uType} : Term uProp ⇒ Term T ⇒ Term T ⇒ Term T
-
-rule if true &t _ → &t
- and if false _ &f → &f
diff --git a/sandbox/cert_f/even.lp b/sandbox/cert_f/even.lp
new file mode 100644
index 0000000..ff5c807
--- /dev/null
+++ b/sandbox/cert_f/even.lp
@@ -0,0 +1,25 @@
+require open encodings.cert_f
+prelude.cert_f.equalities
+prelude.cert_f.naturalnumbers
+adlib.cert_f.nat
+
+symbol mod2: Term nat ⇒ Term nat
+rule mod2 (&n + 2) → mod2 &n
+ and mod2 ( _ + 1) → 1
+ and mod2 0 → 0
+
+definition is_even (n: Term nat) ≔ eq (mod2 n) 0
+
+definition Even ≔ psub nat is_even
+
+definition evenify (n: Term nat) (h: Term (is_even n)) : Term Even ≔
+ pair is_even n h
+
+definition even_to_nat ≔ fst is_even
+
+theorem twice_even_even (n: Term Even):
+ Term (is_even (2 * even_to_nat n))
+proof
+assume n
+simpl
+qed
diff --git a/sandbox/cert_f/rat.lp b/sandbox/cert_f/rat.lp
index 0beee59..82c3cab 100644
--- a/sandbox/cert_f/rat.lp
+++ b/sandbox/cert_f/rat.lp
@@ -7,6 +7,7 @@ constant symbol rat : Univ Type
constant symbol zero : Term rat
symbol frac : Term nat ⇒ Term N.nznat ⇒ Term rat
+set infix 8 "/" ≔ frac
symbol times : @Term Type rat ⇒ @Term Type rat ⇒ @Term Type rat
@@ -22,12 +23,28 @@ rule times (frac &a &b) (frac &c &d) →
(snd N.not_zero &d)))
symbol rateq : Term rat ⇒ Term rat ⇒ Univ Prop
-rule rateq (frac &a &b) (frac &c &d) →
- eq (N.times &a (fst N.not_zero &d)) (N.times (fst N.not_zero &b) &c)
+rule rateq (&a / &b) (&c / &d) →
+ let nzval x ≔ fst N.not_zero x in
+ eq (N.times &a (nzval &d)) (N.times (nzval &b) &c)
definition onz : Term N.nznat ≔ N.nznatc 1 N.one_not_zero
-theorem right_cancellation (a: Term nat) (b: Term N.nznat):
- Term (rateq (times (frac a b) (frac (fst N.not_zero b) onz)) (frac a onz))
+theorem rrefl (a: Term nat) (b: Term N.nznat):
+ Term (rateq (a / b) (a / b))
proof
-admit
+assume a b
+apply N.prod_comm a (fst N.not_zero b)
+qed
+
+theorem one_neutral (a: Term nat) (b: Term N.nznat):
+ Term (rateq (times (a / b) (1 / onz)) (1 / onz))
+proof
+assume a b
+refine N.prod_comm ?p1[a,b] ?p2[a,b]
+qed
+// theorem right_cancellation (a: Term nat) (b: Term N.nznat):
+// Term (rateq (times (a / b) ((fst N.not_zero b) / onz)) (a / onz))
+// proof
+// assume a b
+// refine Term
+// qed
--
GitLab