From 8b0b8d42abc49012ed156b2357123b07cf25b61c Mon Sep 17 00:00:00 2001
From: gabrielhdt <gabrielhondet@gmail.com>
Date: Wed, 22 Apr 2020 13:45:47 +0200
Subject: [PATCH] notation
---
encodings/bool_hol.lp | 2 +-
encodings/bool_pvs.lp | 2 +-
encodings/lhol.lp | 5 +++--
encodings/subtype.lp | 4 ++--
encodings/subtype2.lp | 6 +++---
paper/rat.lp | 15 ++++++---------
prelude/logic.lp | 30 +++++++++++++++---------------
prelude/numbers.lp | 4 ++--
8 files changed, 33 insertions(+), 35 deletions(-)
diff --git a/encodings/bool_hol.lp b/encodings/bool_hol.lp
index 586c9e1..338788c 100644
--- a/encodings/bool_hol.lp
+++ b/encodings/bool_hol.lp
@@ -2,7 +2,7 @@
require open personoj.encodings.lhol
require open personoj.encodings.pvs_cert
-definition false ≔ forall {bool} (λx, x)
+definition false ≔ ∀ {bool} (λx, x)
definition true ≔ impd {false} (λ_, false)
definition not P ≔ impd {P} (λ_, false)
diff --git a/encodings/bool_pvs.lp b/encodings/bool_pvs.lp
index b94bc44..31e9fae 100644
--- a/encodings/bool_pvs.lp
+++ b/encodings/bool_pvs.lp
@@ -3,7 +3,7 @@
require open personoj.encodings.lhol
require open personoj.encodings.pvs_cert
-definition false ≔ forall {bool} (λx, x)
+definition false ≔ ∀ {bool} (λx, x)
definition true ≔ impd {false} (λ_, false)
symbol eq {s: Set}: η s → η s → η bool
diff --git a/encodings/lhol.lp b/encodings/lhol.lp
index 51cf443..7dabafd 100644
--- a/encodings/lhol.lp
+++ b/encodings/lhol.lp
@@ -6,6 +6,7 @@ symbol Bool: TYPE
set declared "Ï•"
set declared "η"
set declared "ε"
+set declared "∀"
injective symbol ϕ: Kind → TYPE
injective symbol η: Set → TYPE
injective symbol ε: Bool → TYPE
@@ -16,11 +17,11 @@ symbol bool: Set
rule ϕ {|set|} ↪ Set
rule η bool ↪ Bool
-symbol forall {x: Set}: (η x → Bool) → Bool
+symbol ∀ {x: Set}: (η x → Bool) → Bool
symbol impd {x: Bool}: (ε x → Bool) → Bool
symbol arrd {x: Set}: (η x → Set) → Set
-rule ε (forall {$X} $P) ↪ Πx: η $X, ε ($P x)
+rule ε (∀ {$X} $P) ↪ Πx: η $X, ε ($P x)
with ε (impd {$H} $P) ↪ Πh: ε $H, ε ($P h)
with η (arrd {$X} $T) ↪ Πx: η $X, η ($T x)
diff --git a/encodings/subtype.lp b/encodings/subtype.lp
index 05fba28..ccf8593 100644
--- a/encodings/subtype.lp
+++ b/encodings/subtype.lp
@@ -16,7 +16,7 @@ symbol S_Restr {a: Set} (p: η a → Bool): ε (psub p ⊑ a)
symbol S_Arr (t u1 u2: Set): ε (u1 ⊑ u2) → ε ((t ~> u1) ⊑ (t ~> u2))
symbol S_Darr (d: Set) (r1: η d → Set) (r2: η d → Set)
- : ε (forall (λx, (r1 x) ⊑ (r2 x))) → ε ((arrd r1) ⊑ (arrd r2))
+ : ε (∀ (λx, (r1 x) ⊑ (r2 x))) → ε ((arrd r1) ⊑ (arrd r2))
// Maximal supertype
symbol μ: Set → Set
@@ -47,7 +47,7 @@ symbol downcast {A: Set} {B: Set} (_: ε (B ⊑ A))
definition ↓ {A} {B} ≔ downcast {A} {B}
set flag "print_implicits" on
-rule π {$T ~> $U} ↪ λx: η $T → η (μ $U), forall (λy, π {$U} (x y))
+rule π {$T ~> $U} ↪ λx: η $T → η (μ $U), ∀(λy, π {$U} (x y))
// rule π {psub {$T} $a} ↪ λx: η (μ $T), π {$T} x
// rule π {psub {$T} $a}
// ↪ λx: η (μ $T), (π {$T} x) ∧ (λy: ε (π {$T} x), $a (↓ {μ $T} {$T} _ x y))
diff --git a/encodings/subtype2.lp b/encodings/subtype2.lp
index 246d456..4204d2a 100644
--- a/encodings/subtype2.lp
+++ b/encodings/subtype2.lp
@@ -25,9 +25,9 @@ definition ↓ {t} ≔ downcast {t}
// rule η (maxcast (maxcast $t)) ↪ η (maxcast $t)
-rule ε (π {$t ~> $u}) ↪ ε (λx: η $t → η (μ $u), forall (λy, π (x y)))
+rule ε (π {$t ~> $u}) ↪ ε (λx: η $t → η (μ $u), ∀ (λy, π (x y)))
with ε (π {psub {$t} $a}) ↪ ε (λx: η (μ $t), (π x) ∧ (λy: ε (π x), $a (↓ x y)))
-with ε (π {arrd $b}) ↪ ε (λx: η (arrd (λx, μ ($b x))), forall (λy, π (x y)))
+with ε (π {arrd $b}) ↪ ε (λx: η (arrd (λx, μ ($b x))), ∀ (λy, π (x y)))
rule ε (π (maxcast _)) ↪ ε true // FIXME: to be justified
@@ -74,7 +74,7 @@ with ε ((arrd {$t1} $u1) ≃ (arrd {$t2} $u2))
↪ ε ((μ $t1 ≃ μ $t2)
∧ (λh,
(eq {μ $t1 ~> bool} π (λx, π (eqcast h x)))
- ∧ (λh', forall
+ ∧ (λh', ∀
(λx: η $t1,
($u1 x) ≃ ($u2 (cast {$t1} {$t2} h x
(comp_same_cstr_cast $t1 $t2 h h' x)))))))
diff --git a/paper/rat.lp b/paper/rat.lp
index cd34b42..6e46ddf 100644
--- a/paper/rat.lp
+++ b/paper/rat.lp
@@ -39,7 +39,7 @@ set infix left 3 "=ℕ" ≔ eqnat
symbol s_not_z: Πx: η ℕ, ε (¬ (Z =ℕ (S x)))
-theorem times_comm: ε (forall (λa, forall (λb, (a * b) =ℕ (b * a))))
+theorem times_comm: ε (∀ (λa, ∀ (λb, (a * b) =ℕ (b * a))))
proof
admit
@@ -61,15 +61,14 @@ rule ($a / $b) =ℚ ($c / $d) ↪ ($a * (fst $d)) =ℕ ((fst $b) * $c)
definition imp P Q ≔ impd {P} (λ_, Q)
set infix left 6 "⊃" ≔ imp
-definition false ≔ forall {bool} (λx, x)
+definition false ≔ ∀ {bool} (λx, x)
theorem nzprod:
- ε (forall
- {â„•*}
- (λx, forall {ℕ*} (λy, {|nznat?|} ((fst x) * (fst y)))))
+ ε (∀ {ℕ*}
+ (λx, ∀ {ℕ*} (λy, {|nznat?|} ((fst x) * (fst y)))))
proof
refine nznat_induction
- (λx, forall (λy: η ℕ*, (Z =ℕ (fst x * fst y)) ⊃ false)) ?xOnz ?xSnz
+ (λx, ∀ (λy: η ℕ*, (Z =ℕ (fst x * fst y)) ⊃ false)) ?xOnz ?xSnz
// x = 1
refine nznat_induction
(λy, (Z =ℕ (fst Onz * fst y)) ⊃ false) ?yOnz ?ySnz
@@ -94,9 +93,7 @@ rule times_rat ($a / $b) ($c / $d) ↪
($a * $c) / (pair denom prf)
theorem right_cancel:
- ε (forall
- (λa, forall
- (λb, eqrat (times_rat (a / b) (fst b / Onz)) (a / Onz))))
+ ε (∀ (λa, ∀ (λb, eqrat (times_rat (a / b) (fst b / Onz)) (a / Onz))))
proof
assume x y
simpl
diff --git a/prelude/logic.lp b/prelude/logic.lp
index ae3b846..0daaf1a 100644
--- a/prelude/logic.lp
+++ b/prelude/logic.lp
@@ -29,9 +29,9 @@ set infix left 2 "≠" ≔ neq
constant symbol bool_exclusive: ε (neq bool false true)
constant
symbol bool_inclusive
- : ε (forall {bool} (λa, ((eq {bool} a false) ∨ (λ_, eq {bool} a true))))
+ : ε (∀ {bool} (λa, ((eq {bool} a false) ∨ (λ_, eq {bool} a true))))
-theorem excluded_middle: ε (forall {bool} (λa, a ∨ (λ_, ¬ a)))
+theorem excluded_middle: ε (∀ {bool} (λa, a ∨ (λ_, ¬ a)))
proof
assume x f
refine f
@@ -43,10 +43,10 @@ qed
definition xor (a b: η bool) ≔ neq bool a b
set flag "print_implicits" on
-theorem xor_def: ε (forall
+theorem xor_def: ε (∀
{bool}
(λa,
- forall
+ ∀
{bool}
(λb, eq {bool} (xor a b)
(if {bool} a (λ_, ¬ b) (λ_, b)))))
@@ -58,7 +58,7 @@ admit
// Quantifier props[t: TYPE]
//
set declared "∃"
-definition ∃ {T: Set} (P: η T → η bool) ≔ ¬ (forall (λx, ¬ (P x)))
+definition ∃ {T: Set} (P: η T → η bool) ≔ ¬ (∀ (λx, ¬ (P x)))
//
// Defined types
@@ -84,37 +84,37 @@ definition SETOF ≔ pred
constant
symbol If_true
: ε (∀B
- (λt, forall
- (λx, forall {t} (λy, if true (λ_, x) (λ_, y) = x))))
+ (λt, ∀
+ (λx, ∀ {t} (λy, if true (λ_, x) (λ_, y) = x))))
constant
symbol If_false
: ε (∀B
- (λt, forall
- (λx, forall {t} (λy, if false (λ_, x) (λ_, y) = y))))
+ (λt, ∀
+ (λx, ∀ {t} (λy, if false (λ_, x) (λ_, y) = y))))
theorem if_same
: ε (∀B (λt,
- forall {bool} (λb, forall (λx: η t,
+ ∀ {bool} (λb, ∀ (λx: η t,
if b (λ_, x) (λ_, x) = x))))
proof
admit
-constant symbol reflexivity_of_equals: ε (∀B (λt, forall (λx: η t, x = x)))
+constant symbol reflexivity_of_equals: ε (∀B (λt, ∀ (λx: η t, x = x)))
set builtin "refl" ≔ reflexivity_of_equals
constant
symbol transitivity_of_equals
: ε (∀B (λt,
- forall
+ ∀
(λx: η t,
- forall
+ ∀
(λy: η t,
- forall
+ ∀
(λz: η t, (x = y) ∧ (λ_, y = z) ⊃ (λ_, x = z))))))
constant
symbol symmetry_of_equals
- : ε (∀B (λt, forall (λx: η t, (forall (λy: η t, (x = y) ⊃ (λ_, y = x))))))
+ : ε (∀B (λt, ∀ (λx: η t, (∀ (λy: η t, (x = y) ⊃ (λ_, y = x))))))
// Not in prelude!
theorem eqind {t} x y: ε (x = y) → Πp: η t → Bool, ε (p y) → ε (p x)
diff --git a/prelude/numbers.lp b/prelude/numbers.lp
index e4854b3..c6e0660 100644
--- a/prelude/numbers.lp
+++ b/prelude/numbers.lp
@@ -30,10 +30,10 @@ set infix 6 "-" ≔ {|-|}
// rule ty_plus numfield numfield ↪ numfield
constant
-symbol commutative_add : ε (forall (λx, forall (λy, x + y = y + x)))
+symbol commutative_add : ε (∀ (λx, ∀ (λy, x + y = y + x)))
constant
symbol associative_add
- : ε (forall (λx, forall (λy, forall (λz, x + (y + z) = (x + y) + z))))
+ : ε (∀ (λx, ∀ (λy, ∀ (λz, x + (y + z) = (x + y) + z))))
// FIXME add a cast on zero?
// symbol identity_add (x: Term numfield): Term (x + zero = x)
--
GitLab