Cleaning

adlib/booleans.lp

-require open
-  personoj.encodings.lhol
-  personoj.encodings.pvs_cert
-  personoj.encodings.booleans
-
-definition false ≔ forall {bool} (λx, x)
-definition true ≔ impd {false} (λ_, false)
-
-definition imp P Q ≔ impd {P} (λ_, Q)
-
-definition bnot P ≔ impd {P} (λ_, false)
-definition band P Q ≔ bnot (imp P (bnot Q))
-definition bor P Q ≔ imp (bnot P) Q
-set prefix 5 "¬" ≔ bnot
-set infix 6 "∧" ≔ band
-set infix 5 "∨" ≔ bor
-
-definition biff P Q ≔ (imp P Q) ∧ (imp Q P)
-set infix 7 "⇔" ≔ biff
-
-definition when P Q ≔ imp Q P
-
-set builtin "imp" ≔ imp
-set builtin "not" ≔ bnot
-set builtin "and" ≔ band
-set builtin "or"  ≔ bor

adlib/bootstrap.lp

-require open personoj.encodings.cert_f
-
-definition bool ≔ uProp
-definition false ≔ prod bool (λ x, x)
-definition true ≔ prod false (λ _, false)
-
-definition imp (P Q: Term uProp) ≔ prod P (λ_, Q)
-definition forall {T: Term uType} (P: Term T → Term bool) ≔ prod T P
-
-definition bnot (P: Term uProp) ≔ prod P (λ _, false)
-set prefix 5 "¬" ≔ bnot
-
-definition band P Q ≔ bnot (imp P (bnot Q))
-set infix 6 "∧" ≔ band
-definition bor P Q ≔ imp (bnot P) Q
-set infix 5 "∨" ≔ bor
-
-definition biff P Q ≔ (imp P Q) ∧ (imp Q P)
-set infix 7 "⇔" ≔ biff
-
-definition when P Q ≔ imp Q P
-
-set builtin "bot" ≔ false
-set builtin "top" ≔ true
-set builtin "imp" ≔ imp
-set builtin "and" ≔ band
-set builtin "or"  ≔ bor
-set builtin "not" ≔ bnot
-
-// Defined here because ⊑ needs it.
-symbol eq {T: Term uType}: Term T → Term T → Term bool
-set infix 5 "=" ≔ eq
-// set builtin "eq" ≔ eq

adlib/induction.lp

-require open personoj.encodings.cert_f
-personoj.adlib.bootstrap
-
-// 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)

adlib/subtype.lp

-require open personoj.encodings.cert_f
-        personoj.adlib.bootstrap
-
-// A la rewriting logic
-rule Psub {$A} _ ⊑ $A ↪ true
- and $A ⊑ $A          ↪ true
-
-// [eqroot T U] reduces to [true] if [T] and [U] have the same root
-symbol eqroot: Term uType → Term uType → Term uProp
-rule eqroot $X $X            ↪ true // NOTE: non linear
- and eqroot (Psub {$T} _) $U ↪ eqroot $T $U
- and eqroot $T (Psub {$U} _) ↪ eqroot $T $U
-
-symbol eqtype: Term uType → Term uType → Term uProp
-
-symbol refl T: Term (T ⊑ T)
-symbol restr T P: Term (Psub {T} P ⊑ T)
-
-symbol trans (T U V: Term uType):
-  Term (T ⊑ U) → Term (U ⊑ V) → Term (T ⊑ V)
-
-// [sub {U} P T μ π ρ] proves that, given type [U], [P] predicate from [U],
-// type [T],
-// - proof [μ] that [T] has the same root as [U];
-// - proof [π] that [T] is a sub-type of [U];
-// - proof [ρ] that any element of [T] verifies [P];
-// [T] is a sub-type of [{x: U | P}].
-symbol sub {U: Term uType} (P: Term U → Term bool) (T: Term uType)
-  (_: Term (eqroot T U)) (pr: Term (T ⊑ U)):
-  Term (forall (λx: Term T, P (↑ U pr x))) → Term (T ⊑ Psub P)
-
-// symbol sub {T S: Term uType}
-//   (P: Term T → Term bool) (Q: Term S → Term bool)
-//   (psubt: Term (T ⊑ S)): // Proof of T ⊑ S
-//   Term (forall (λx, imp (P x) (Q (↑ S psubt x)))) →
-//   Term (Psub T P ⊑ Psub S Q)
-
-// Transitivity of the cast
-rule ↑ {$U} $V $pruv (↑ {$T} $U $prtu $x) ↪
-  ↑ {$T} $V (trans $T $U $V $prtu $pruv) $x
-
-constant symbol cast_trans (A B C: Term uType) (prab: Term (A ⊑ B))
-  (prbc: Term (B ⊑ C)) (x: Term A)
-  : Term (eq (↑ {B} C prbc (↑ {A} B prab x))
-  (↑ {A} C (trans A B C prab prbc) x))

alternatives/adlib/core/nat.lp

-require open encodings.pvs_core prelude.core.notequal
-// Not part of prelude as integers are built in pvs
-
-constant symbol int : Type
-symbol zero : eta int
-symbol succ (_: eta int) : eta int
-
-set builtin "0" ≔ zero
-set builtin "+1" ≔ succ

alternatives/adlib/core/nat_ops.lp

-require open encodings.pvs_core prelude.core.notequal adlib.core.nat
-prelude.core.equalities
-
-symbol times : eta int → eta int → eta int
-rule times $n 1  ↪ $n
-
-set infix left 6 "*" ≔ times
-
-// x =/= 0 ∧ y =/= 0 → x * y =/= 0
-symbol prod_not_zero (x y: η int) :
-  ε (neq x 0) → ε (neq y 0) → ε (neq (x * y) 0)
-
-symbol prod_comm (x y : η int) : ε (eq (x * y) (y * x))

alternatives/prelude/core/boolean_props.lp

-require open encodings.pvs_core
-prelude.core.booleans prelude.core.equalities prelude.core.if_def
-
-theorem excluded_middle : Π A : eta bool, eps (bor A (bnot A))
-proof
-admit

alternatives/prelude/core/booleans.lp

-require open encodings.pvs_core
-
-set builtin "T" ≔ eta
-set builtin "P" ≔ eps
-
-// booleans
-definition bool ≔ Prop
-
-// Minimal definitions, only the implication is primitive
-definition false ≔ all bool (λ p : η bool, p)
-definition true ≔ imp false false
-
-definition bnot (P: η bool) ≔ imp P false
-set prefix 5 "¬" ≔ bnot
-definition band (P Q: η bool) ≔ ¬ (imp P (¬ Q))
-definition bor (P Q: η bool) ≔ (imp (¬ P) Q)
-set infix 6 "∧" ≔ band
-set infix 5 "∨" ≔ bor
-definition biff (P Q: η bool) ≔ (imp P Q) ∧ (imp Q P)

alternatives/prelude/core/equalities.lp

-require open encodings.pvs_core prelude.core.booleans
-
-symbol eq {T : Type} : eta T → eta T → eta bool

alternatives/prelude/core/if_def.lp

-require open encodings.pvs_core prelude.core.booleans prelude.core.equalities
-prelude.core.notequal
-
-symbol if {T:Type}: η bool → eta T → eta T → eta T

alternatives/prelude/core/notequal.lp

-require open encodings.pvs_core prelude.core.booleans prelude.core.equalities
-
-definition neq {T: Type} (x: eta T) (y: eta T) ≔ bnot (eq x y)

alternatives/prelude/core/quantifier_props.lp

-require open encodings.pvs_core prelude.core.booleans prelude.core.equalities
-
-definition exists {T: Type} (p : eta T → eta bool) ≔
-    (bnot (all T (λ x, (bnot (p x)))))
-
-set declared "∃"
-definition ∃ {T: Type} ≔ @exists T
-
-theorem exists_not (T: Type) (p: η T → η bool):
-  ε (eq (∃ (λ x, ¬ (p x))) (¬ (all T p)))
-proof
-admit
-
-theorem exists_or (T: Type) (p q: η T → η bool):
-  ε (eq (∃ (λ x, (p x) ∨ (q x))) ((∃ p) ∨ (∃ q)))
-proof admit

alternatives/prelude/core/xor_def.lp

-require open encodings.pvs_core prelude.core.booleans prelude.core.notequal
-prelude.core.equalities prelude.core.if_def
-
-definition xor (A : η bool) (B : η bool) ≔ neq A B
-
-theorem xor_def (A B: η bool) : ε (eq (xor A B) (if A (¬ B) B))
-proof admit

alternatives/sandbox/core/rat.lp

-require open pvs_core prelude.booleans prelude.equalities prelude.notequal
-require open prelude.nat
-require prelude.nat_ops as N
-
-constant symbol rat : Type
-constant symbol zrat : η rat
-
-definition intnz ≔ psub int (λ x, neq 0 x)
-
-symbol frac : η int → η intnz → η rat
-
-symbol times : η rat → η rat → η rat
-set infix 5 "*" ≔ times
-rule times (frac $a $b) (frac $c $d) ↪ frac (N.times $a $c) (N.times $b $d)
-
-symbol rateq : η rat → η rat → η bool
-rule rateq (frac $a $b) (frac $c $d) ↪ eq (N.times $a $d) (N.times $b $c)
-
-theorem right_cancellation (a : η int) (b : η intnz) :
-  ε (rateq ((frac a b) * (frac b 1)) (frac a 1))
-  proof
-  admit

alternatives/sandbox/core/rat_explicit.lp

-require open encodings.pvs_core prelude.core.booleans prelude.core.equalities
-prelude.core.notequal adlib.core.nat
-require adlib.core.nat_ops as N
-
-constant symbol rat : Type
-constant symbol zero : η rat
-
-symbol frac (_ m : η int) (pi : ε (neq m 0)) : η rat
-
-symbol div : η rat → η rat → η rat
-symbol times : η rat → η rat → η rat
-set infix 5 "*" ≔ times
-set infix 6 "/" ≔ div
-
-rule times (frac $A $B $X) (frac $C $D $Y) ↪
-  frac (N.times $A $C) (N.times $B $D) (N.prod_not_zero $B $D $X $Y)
-
-symbol rateq : η rat → η rat → η Prop
-rule rateq (frac $A $B _) (frac $C $D _) ↪
-  eq (N.times $A $D) (N.times $B $C)
-
-// (a/b) * (b/1) = (a/1)
-theorem right_cancellation (a b : η int) (pi : ε (neq b 0)) (pi' : ε (neq 1 0)):
-  ε (rateq ((frac a b pi) * (frac b 1 pi')) (frac a 1 pi'))
-proof
-assume a b pi pi'
-simpl
-refine N.prod_comm a b
-qed

sandbox/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/ifs.lp

-require open personoj.encodings.lhol
-  personoj.encodings.pvs_cert
-  personoj.encodings.booleans
-require personoj.encodings.deferred as Deferred
-require open personoj.encodings.subtype //FIXME: why must it be the last import?
-
-symbol if {U: Set} {V: Set} (S: Set)
-: ε (U ⊑ S) → ε (V ⊑ S) → Bool → η U → η V → η S
-
-symbol lif {U: Set} {V: Set} (S: Set)
-: Deferred.p (U ⊑ S) → Deferred.p (V ⊑ S) → Bool → Deferred.t U → Deferred.t V → η S
-
-// lazy if
-set flag "print_implicits" on
-rule lif _ $pr _ true $t _ ↪ ↑ (Deferred.unquote_p $pr) (Deferred.unquote $t)
-rule lif _ _ $pr false _ $f ↪ ↑ (Deferred.unquote_p $pr) (Deferred.unquote $f)
-
-// The if is lazy, that is, the expression [if true 2 (1/0)] must type check and
-// return 2. For this, we use the [Deferred.t] datatype. But remember that [if]
-// is typed by a super type of [2] and [1/0]. This super type is provided as
-// argument, and the types of the expressions must be verified to be sub-types
-// of this super-types. Since these arguments are deferred and can be ill-typed,
-// we want to defer the verification of sub-type as well. Therefore, we
-// introduce the [lifSet] type to type the [lif].
-// [lifset $T $F $S p] reduces to the type of the function that maps a proof of
-// $T is a sub-type of $S to $S if [p] is true and the function that maps a
-// proof of $F is a sub-type of $S if [p] is false.
-// The result of [lif S true e1 e2] is the function that maps the proof of
-// sub-typing [Te1 ⊑ S] to the evaluation (or unquoting) of [e1].
-type λ (T S: Set), ε (T ⊑ S) → η S
-symbol lifSet (T U S: Set): Bool → TYPE
-symbol tt: Bool
-symbol ff: Bool
-rule lifSet $U _ $S true ↪ ε ($U ⊑ $S) → η $S
-rule lifSet _ $F $S false ↪ ε ($F ⊑ $S) → η $S
-
-compute λ(U V S: Set), lifSet U V S tt
-
-symbol lifn {U: Set} {V: Set} (S: Set) (p: Bool)
-: Deferred.t U → Deferred.t V → lifSet U V S p
-
-rule lifn {$U} {$V} $S true $t $f ↪ λh:ε ($U ⊑ $S), ↑ {$U} {$S} h (Deferred.unquote $t)
-
-symbol if3 {u: Set} {v: Set} (s: Set) (_: ε (u ⊑ s)) (_: ε (v ⊑ s)) (p: Bool):
-  (ε p → η u) → (ε (¬ p) → η v) → η s
-
-rule if3 $s $pr _ true $bh _ ↪ ↑ $pr ($bh (λx, x))
- and if3 $s _ $pr false _ $bh ↪ ↑ $pr ($bh (λx, x))

sandbox/nat.lp

-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
-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 ((x * y) = (y * x))
-
-
-//
-// Non zero naturals
-//
-
-definition not_zero ≔ neq 0
-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
-
-// Constructor of 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):
-  Πn, Term (P 0) → Term (P (n + 1)) → Πm, Term (P m)
-
-// Divisions
-definition div (x y: Term Nat) ≔ ∃ (λk, x * k = y)
-definition even (x: Term Nat) ≔ div 2 x
-definition Even ≔ Psub even
-
-theorem even_stable_double: Πx: Term Even, Term (even (2 * (fst x)))
-proof
-    assume x h
-    refine (h (fst x) _)
-    simpl
-    refine reflexivity_of_equal _ ((fst x) + (fst x))
-qed
-
-symbol surjective_pairing T (p: Term T → Term bool):
-       Πx: Term (Psub p), Term (pair p (fst x) (snd x) = x)
-
-//symbol app_thm (D R: Term uType) (f: Term (D ~> R))
-//     : Πx y: Term D, Term (x = y) → Term (f x = f y)
-
-theorem fst_injective: Πx y: Term Even, Term (fst x = fst y) → Term (x = y)
-proof
-    assume x y h
-    refine transitivity_of_equal Even x (pair even (fst x) (snd x)) y _
-    assume h0
-    refine h0 ?P0[x,y,h,h0] _
-
-    // Proof of P0 that x = pair even (fst x) (snd x)
-    refine symmetry_of_equal Even (pair even (fst x) (snd x)) x _
-    refine surjective_pairing _ even x
-
-    refine transitivity_of_equal Even (pair even (fst x) (snd x)) (pair even (fst y) (snd y)) y _
-    assume h1
-    refine h1 _ _
-    focus 1
-    refine surjective_pairing _ even y
-
-abort
-
-rule $x = $x ↪ true
-theorem prf_irrelevance T (p: Term T → Term bool)
-: Π(x: Term T) (pr: Term (p x)) (pr': Term (p x)), Term (pair p x pr = pair p x pr')
-proof
-    assume T p x pr0 pr1
-    simpl
-    assume h
-    refine h
-qed

sandbox/rat.lp

-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 : Term uType
-constant symbol zero : Term Rat
-
-symbol rat : Term N.Nat → Term N.Nznat → Term Rat
-set infix 8 "/" ≔ rat
-
-symbol times : Term Rat → Term Rat → Term Rat
-
-rule times (rat $a $b) (rat $c $d) ↪
-  let bv ≔ fst $b in
-  let dv ≔ fst $d in
-  rat
-   (N.times $a $c)
-   (N.nznat
-    (N.times bv dv)
-    (N.prod_not_zero bv dv
-     (snd $b)
-     (snd $d)))
-
-symbol rateq : Term Rat → Term Rat → Term bool
-rule rateq ($a / $b) ($c / $d) ↪
-  let nzval x ≔ fst x in
-  (N.times $a (nzval $d)) = (N.times (nzval $b) $c)
-
-definition onz : Term N.Nznat ≔ N.nznat 1 N.one_not_zero
-
-// NOTE: we use this rewriting rule because in the proof below, calling simpl
-// causes protected [opair] to appear, and we cannot use refl since it requires
-// the user to input the protected opair, which is forbidden.
-// Perhaps using [hints] could help, using [refl Nat _] and the unification
-// engine would instantiate _ accordingly, but it is not likely since it is
-// based on non linearity, and hints are linear.
-// We rather reduce the proof to the trivial proof
-rule $x = $x ↪ true
-theorem right_cancellation (a: Term N.Nat) (b: Term N.Nznat):
-    Term (rateq (times (a / b) ((fst b) / onz)) (a / onz))
-proof
-    assume a b
-    simpl
-    refine N.prod_comm a (fst b)
-qed