more implicits on fst, moved nat

encodings/cert_f.lp

@@ -43,14 +43,14 @@ constant symbol Psub {T: Term uType}: (Term T ⇒ Term uProp) ⇒ Term uType
 // Γ ⊢ M : { v : T | P }
 // —————————————————————PROJl
 //      Γ ⊢ fst(M) : T
-symbol fst {T: Univ Type} (P: Term T ⇒ Univ Prop): Term (Psub P) ⇒ Term T
+symbol fst {T: Univ Type} {P: Term T ⇒ Univ Prop}: Term (Psub P) ⇒ Term T
 
 //  Γ ⊢ M : { v : T | P }
 // ——————————————————————————PROJr
 // Γ ⊢ snd(M) : P[v ≔ fst(M)]
 constant symbol snd {T: Univ Type} {P: Term T ⇒ Univ Prop}
   (M: Term (Psub P)):
-  Term (P (fst P M))
+  Term (P (fst M))
 
 // An inhabitant of a predicate subtype, that is, a pair of
 // an element and the proof that it satisfies the predicate
@@ -60,7 +60,7 @@ constant symbol snd {T: Univ Type} {P: Term T ⇒ Univ Prop}
 symbol pair {T: Univ Type} (P: Term T ⇒ Univ Prop) (M: Term T):
   Term (P M) ⇒ Term (Psub P)
 
-rule fst _ (pair _ &M _) → &M
+rule fst (pair _ &M _) → &M
 
 // opair is a pair forgetting its snd argument
 protected symbol opair (T: Univ Type) (P: Term T ⇒ Univ Prop) (M: Term T):
@@ -79,7 +79,7 @@ set declared "↑"
 symbol ↑ {T: Term uType} (U: Term uType): Term (T ⊑ U) ⇒ Term T ⇒ Term U
 rule ↑ {&T} &T _ &x → &x // Identity cast
 // NOTE: a cast from a type [{x: A | P}] to type [A] is a [fst],
- and ↑ {Psub {&T} &P} &T _ → fst &P
+and ↑ {Psub {&T} &P} &T _ → fst {&T} {&P}
 // and a "downcast" is the pair constructor
 set declared "↓"
 

adlib/nat.lp → sandbox/nat.lp

-require open encodings.cert_f adlib.cert_f.booleans
-prelude.cert_f.logic
-
-constant symbol nat: Term uType
-injective symbol succ: Term nat ⇒ Term nat
-constant symbol zero: Term nat
+require open
+    personoj.encodings.cert_f
+    personoj.adlib.bootstrap
+    personoj.prelude.logic
+
+constant symbol Nat: Term uType
+injective symbol succ: Term Nat ⇒ Term Nat
+constant symbol zero: Term Nat
 set builtin "0" ≔ zero
 set builtin "+1" ≔ succ
 
-symbol times : Term nat ⇒ Term nat ⇒ Term nat
-symbol plus : Term nat ⇒ Term nat ⇒ Term nat
+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
 
@@ -22,7 +24,7 @@ rule (succ &n) *       &m  → &n * &m + &m
  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))
+symbol prod_comm (x y: Term Nat): Term (eq (times x y) (times y x))
 
 
 //
@@ -30,16 +32,16 @@ symbol prod_comm (x y: Term nat): Term (eq (times x y) (times y x))
 //
 
 definition not_zero ≔ neq 0
-symbol prod_not_zero (x y: Term nat):
+symbol prod_not_zero (x y: Term Nat):
   Term (not_zero x) ⇒ Term (not_zero y) ⇒ Term (not_zero (times x y))
 
-definition nznat ≔ Psub not_zero
+definition Nznat ≔ Psub not_zero
 
 // Constructor of nznat
-definition nznatc (x: Term nat) (h: Term (not_zero x)) : Term nznat ≔
+definition nznat (x: Term Nat) (h: Term (not_zero x)) : Term Nznat ≔
   pair not_zero x h
 
 symbol one_not_zero: Term (not_zero 1)
 
-symbol induction (P: Term nat ⇒ Term bool):
+symbol induction (P: Term Nat ⇒ Term bool):
   ∀n, Term (P 0) ⇒ Term (P (n + 1)) ⇒ ∀m, Term (P m)

sandbox/rat.lp

-require open encodings.cert_f adlib.cert_f.booleans
-prelude.cert_f.logic
-require adlib.cert_f.nat as N
+require open
+    personoj.encodings.cert_f
+    personoj.adlib.bootstrap
+    personoj.prelude.logic
+
+require personoj.sandbox.nat as N
 
 set builtin "0" ≔ N.zero
 set builtin "+1" ≔ N.succ
 
-constant symbol rat : Univ Type
-constant symbol zero : Term rat
+constant symbol Rat : Term uType
+constant symbol zero : Term Rat
+
+symbol rat : Term N.Nat ⇒ Term N.Nznat ⇒ Term Rat
+set infix 8 "/" ≔ rat
 
-symbol frac : Term N.nat ⇒ Term N.nznat ⇒ Term rat
-set infix 8 "/" ≔ frac
+symbol times : Term Rat ⇒ Term Rat ⇒ Term Rat
 
-symbol times : Term rat ⇒ Term rat ⇒ Term rat
+type λx: Term N.Nznat, fst x
 
-rule times (frac &a &b) (frac &c &d) →
-  let bv ≔ fst N.not_zero &b in
-  let dv ≔ fst N.not_zero &d in
-  frac
+rule times (rat &a &b) (rat &c &d) →
+  let bv ≔ fst &b in
+  let dv ≔ fst &d in
+  rat
    (N.times &a &c)
-   (N.nznatc
+   (N.nznat
     (N.times bv dv)
     (N.prod_not_zero bv dv
-     (snd N.not_zero &b)
-     (snd N.not_zero &d)))
+     (snd &b)
+     (snd &d)))
 
-symbol rateq : Term rat ⇒ Term rat ⇒ Univ Prop
+symbol rateq : Term Rat ⇒ Term Rat ⇒ Term bool
 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)
+  let nzval x ≔ fst x in
+  (N.times &a (nzval &d)) = (N.times (nzval &b) &c)
 
-definition onz : Term N.nznat ≔ N.nznatc 1 N.one_not_zero
+definition onz : Term N.Nznat ≔ N.nznat 1 N.one_not_zero
 
-theorem rrefl (a: Term N.nat) (b: Term N.nznat):
+theorem rrefl (a: Term N.Nat) (b: Term N.Nznat):
   Term (rateq (a / b) (a / b))
 proof
-assume a b
-apply N.prod_comm a (fst N.not_zero b)
+    assume a b
+    apply N.prod_comm a (fst b)
 qed
 
 // theorem one_neutral (a: Term N.nat) (b: Term N.nznat):
 //   Term (rateq (times (a / b) (1 / onz)) (1 / onz))
 // proof
 // qed
-type Term (N.nznat ⊑ N.nat)
-type λ(b: Term N.nznat) (pr: Term (N.nznat ⊑ N.nat)),
-  @↑ N.nznat N.nat pr b
-// FIXME explicitness required
-theorem right_cancellation (a: Term N.nat) (b: Term N.nznat)
-  (pr: Term (N.nznat ⊑ N.nat)):
-  Term (rateq (times (a / b) ((@↑ N.nznat N.nat pr b) / onz)) (a / onz))
+type Term (N.Nznat ⊑ N.Nat)
+type λ(b: Term N.Nznat) (pr: Term (N.Nznat ⊑ N.Nat)),
+  ↑ N.Nat pr b
+theorem right_cancellation (a: Term N.Nat) (b: Term N.Nznat)
+  (pr: Term (N.Nznat ⊑ N.Nat)):
+  Term (rateq (times (a / b) ((↑ N.Nat pr b) / onz)) (a / onz))
 proof
 qed
 // Should generate a TCC to provide [pr]
+
+// theorem right_cancel (a b: Term N.Nat) ()