more

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 ≔

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)
 

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

prelude/cert_f/equality_props.lp

+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)

prelude/cert_f/if_def.lp

 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

sandbox/cert_f/even.lp

+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

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