From ada38d08f896ba7e80f6a2df80f1cd9fff7ca09a Mon Sep 17 00:00:00 2001 From: NotBad4U Date: Thu, 17 Sep 2026 17:07:12 +0200 Subject: [PATCH 01/13] Add lemmas and definitions from Alethe development MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Bool.lp: imp, xorb, if-then-else lemmas Epsilon.lp: εₑ HOL.lp: transport List.lp: foldl/foldr, mergesort and its correctness Nat.lp: parity, div2, bitwise ops, strong induction Pos.lp: multiplication lemmas Prod.lp: sum type, dependent pairs, product lemmas Z.lp: multiplication, power, comparison lemmas --- Bool.lp | 174 ++++++++++++++ Epsilon.lp | 10 +- HOL.lp | 7 +- List.lp | 250 ++++++++++++++++++- Nat.lp | 520 ++++++++++++++++++++++++++++++++++++---- Pos.lp | 128 +++++++++- Prod.lp | 284 +++++++++++++++++++++- Z.lp | 685 +++++++++++++++++++++++++++++++++++++++++++++++++---- 8 files changed, 1964 insertions(+), 94 deletions(-) diff --git a/Bool.lp b/Bool.lp index 8cac791..ad48515 100644 --- a/Bool.lp +++ b/Bool.lp @@ -104,6 +104,20 @@ begin { simplify; assume h0 h1; refine h1 } end; +opaque symbol notK b : π (not (not b) = b) ≔ +begin + induction + { reflexivity } + { reflexivity } +end; + +opaque symbol negb_false_eq_true b : π (not b = false ⇔ b = true) ≔ +begin +induction +{simplify; apply ∧ᵢ { assume h; reflexivity } { assume h; reflexivity }} +{simplify; apply ∧ᵢ { assume h; apply ⊥ₑ (true≠false h) } { assume h; apply ⊥ₑ (false≠true h) }} +end; + // or symbol or : 𝔹 → 𝔹 → 𝔹; @@ -129,6 +143,65 @@ begin {reflexivity} end; +// imp + +symbol imp : 𝔹 → 𝔹 → 𝔹; + +notation imp infix left 20; + +rule true imp true ↪ true +with true imp false ↪ false +with false imp true ↪ true +with false imp false ↪ true; + +opaque symbol ⇒_istrue [p q : 𝔹] : π(p imp q) → π(p ⇒ q) ≔ +begin + induction + { induction + { + simplify; + assume h1; refine (λ x, x) + } + { + simplify; assume h1 h2; refine h1 + } + } + { + induction + { + simplify; + assume h1 h2; apply h1 + } + { + simplify; + assume h1; refine (λ x, x) + } + } +end; + +opaque symbol istrue_imp [p q : 𝔹] : π(p ⇒ q) → π(p imp q) ≔ +begin + induction + { induction + { assume h; apply ⊤ᵢ } + { assume h; apply h ⊤ᵢ } + } + { induction + { assume h; apply ⊤ᵢ } + { assume h; apply ⊤ᵢ } + } +end; + +opaque symbol impᵢ [p q : 𝔹] : (π p → π q) → π (p imp q) ≔ +begin + assume p q h; apply @istrue_imp p q h; +end; + +opaque symbol impₑ [p q : 𝔹] : π (p imp q) → π p → π q ≔ +begin + assume p q h; refine @⇒_istrue p q h; +end; + opaque symbol ∨_istrue [p q : 𝔹] : π(p or q) → π(p ∨ q) ≔ begin induction @@ -226,9 +299,110 @@ begin { assume q i; apply ⊥ₑ i; } end; +// xorb + +symbol xorb : 𝔹 → 𝔹 → 𝔹; + +notation xorb infix left 22; + +rule false xorb false ↪ false +with false xorb true ↪ true +with true xorb false ↪ true +with true xorb true ↪ false; + +opaque symbol xorbᵢ₁ [p q : 𝔹] : π p → π (not q) → π (p xorb q) ≔ +begin + induction + { induction + { simplify; assume h i; apply i } + { simplify; assume h i; apply ⊤ᵢ } + } + { induction + { simplify; assume h i; apply ⊥ₑ h } + { simplify; assume h i; apply ⊥ₑ h } + } +end; + +opaque symbol xorbᵢ₂ [p q : 𝔹] : π (not p) → π q → π (p xorb q) ≔ +begin + induction + { induction + { simplify; assume h i; apply ⊥ₑ h } + { simplify; assume h i; apply ⊥ₑ h } + } + { induction + { simplify; assume h i; apply ⊤ᵢ } + { simplify; assume h i; apply ⊥ₑ i } + } +end; + +opaque symbol xorbₑ [p q : 𝔹] (r : 𝔹) : + π (p xorb q) → (π p → π (not q) → π r) → (π (not p) → π q → π r) → π r ≔ +begin + induction + { induction + { simplify; assume r h h1 h2; apply ⊥ₑ h } + { simplify; assume r h h1 h2; apply h1 ⊤ᵢ ⊤ᵢ } + } + { induction + { simplify; assume r h h1 h2; apply h2 ⊤ᵢ ⊤ᵢ } + { simplify; assume r h h1 h2; apply ⊥ₑ h } + } +end; + // if-then-else symbol if : 𝔹 → Π [a], τ a → τ a → τ a; rule if true $x _ ↪ $x with if false _ $y ↪ $y; + +opaque symbol if_true [a] (x y : τ a) : π (if true x y = x) ≔ +begin + assume a x y; reflexivity +end; + +opaque symbol if_false [a] (x y : τ a) : π (if false x y = y) ≔ +begin + assume a x y; reflexivity +end; + +opaque symbol if_same b [a] (x : τ a) : π (if b x x = x) ≔ +begin + assume b a x; + refine ∨ₑ (case_𝔹 b) _ _ + { assume h; rewrite h; reflexivity } + { assume h; rewrite h; reflexivity } +end; + +opaque symbol if_id b : π (if b true false = b) ≔ +begin + induction + { reflexivity } + { reflexivity } +end; + +opaque symbol if_not b [a] (x y : τ a) : π (if (not b) x y = if b y x) ≔ +begin + assume b a x y; + refine ∨ₑ (case_𝔹 b) _ _ + { assume h; rewrite h; reflexivity } + { assume h; rewrite h; reflexivity } +end; + +opaque symbol if_istrue [b : 𝔹] [a] (x y : τ a) : π b → π (if b x y = x) ≔ +begin + assume b a x y h; + refine ∨ₑ (case_𝔹 b) _ _ + { assume h1; rewrite h1; reflexivity } + { assume h1; apply ⊥ₑ (false=¬istrue h1 h) } +end; + +opaque symbol if_isfalse [b : 𝔹] [a] (x y : τ a) : π (not b) → π (if b x y = y) ≔ +begin + assume b a x y h; + refine ∨ₑ (case_𝔹 b) _ _ + { assume h1; apply ⊥ₑ (istrue_not h (true=istrue h1)) } + { assume h1; rewrite h1; reflexivity } +end; + diff --git a/Epsilon.lp b/Epsilon.lp index fcb100e..a00783e 100644 --- a/Epsilon.lp +++ b/Epsilon.lp @@ -1,4 +1,12 @@ -require open Stdlib.FOL; +require open Stdlib.FOL Stdlib.FunExt Stdlib.Impred; symbol ε [a:Set] : (τ a → Prop) → τ a; symbol εᵢ [a:Set] (p:τ a → Prop) : π (∃ p) → π (p (ε p)); + +opaque symbol εₑ [a:Set] (p:τ a → Prop) : π (p (ε p)) → π (∃ p) ≔ +begin + assume a p h; + have e : π ((λ x, p x) = p) { refine funExt (λ x, p x) p (λ x, eq_refl (p x)) }; + rewrite left e; + refine ∃ᵢ (ε p) h +end; \ No newline at end of file diff --git a/HOL.lp b/HOL.lp index 08dd3bf..0204d0d 100644 --- a/HOL.lp +++ b/HOL.lp @@ -1,4 +1,4 @@ -require open Stdlib.Set; +require open Stdlib.Set Stdlib.Eq; constant symbol ⤳ : Set → Set → Set; // \leadsto @@ -18,3 +18,8 @@ rule τ ($a ⤳d λ x,$b.[x]) ↪ Π x:τ $a, τ $b.[x]; symbol ∘ [a b c] : τ (b ⤳ c) → τ (a ⤳ b) → τ a → τ c ≔ λ g f x, g (f x); notation ∘ infix 20; + +symbol transport [a] (p: τ a → Set) [x y: τ a] : π (x = y) → τ (p x) → τ (p y); + +rule @transport _ _ $x $x _ $u ↪ $u +with @transport _ (λ _, _) _ _ _ $u ↪ $u; diff --git a/List.lp b/List.lp index 2b8a7d3..757d0d8 100644 --- a/List.lp +++ b/List.lp @@ -204,7 +204,7 @@ protected with nosimpl. An example of use can be found in fingraph theorem orbitPcycle. */ -require open Stdlib.Nat Stdlib.Prod; +require open Stdlib.Nat Stdlib.Prod Stdlib.HOL; (a:Set) inductive 𝕃:TYPE ≔ | □ : 𝕃 a // \Box @@ -1920,3 +1920,251 @@ rule prodn □ ↪ 1 with prodn ($x ⸬ $l) ↪ $x * prodn $l; assert ⊢ prodn (3 ⸬ 2 ⸬ 1 ⸬ □) ≡ 3 !; + +// foldl + +symbol foldl [a b] : τ (a ⤳ b ⤳ a) → τ a → 𝕃 b → τ a; + +rule foldl _ $acc □ ↪ $acc +with foldl $op $acc ($h ⸬ $tl) ↪ foldl $op ($op $acc $h) $tl; + +assert ⊢ sumn (3 ⸬ 2 ⸬ 1 ⸬ □) ≡ foldl (+) 0 (3 ⸬ 2 ⸬ 1 ⸬ □); + +// foldr + +symbol foldr [a b] : τ (b ⤳ a ⤳ a) → τ a → 𝕃 b → τ a; + +rule foldr _ $acc □ ↪ $acc +with foldr $op $acc ($h ⸬ $tl) ↪ $op $h (foldr $op $acc $tl); + +assert ⊢ sumn (3 ⸬ 2 ⸬ 1 ⸬ □) ≡ foldr (+) 0 (3 ⸬ 2 ⸬ 1 ⸬ □); + +// Sorting algorithm Merge Sort + +symbol split [a: Set] (l : τ (list a)): τ(list a × list a); +rule split □ ↪ (□ ‚ □) +with split ($x ⸬ □) ↪ (($x ⸬ □) ‚ □) +with split ($x ⸬ $y ⸬ $l) ↪ + let res ≔ (split $l) in + ($x ⸬ (res ₁)) ‚ ($y ⸬ (res ₂)); + +// merge and mergesort are parametrised by a boolean ordering on the elements + +symbol merge [a] : (τ a → τ a → 𝔹) → 𝕃 a → 𝕃 a → 𝕃 a; +rule merge _ □ $l2 ↪ $l2 +with merge _ $l1 □ ↪ $l1 +with merge $ble ($a1 ⸬ $l1') ($a2 ⸬ $l2') ↪ + if ($ble $a1 $a2) + ($a1 ⸬ merge $ble $l1' ($a2 ⸬ $l2')) + ($a2 ⸬ merge $ble ($a1 ⸬ $l1') $l2'); + +symbol mergesort [a] : (τ a → τ a → 𝔹) → 𝕃 a → 𝕃 a; +rule mergesort _ □ ↪ □ +with mergesort _ ($x ⸬ □) ↪ ($x ⸬ □) +with mergesort $ble ($x ⸬ $y ⸬ $l) ↪ + let s ≔ split ($x ⸬ $y ⸬ $l) in + let l1 ≔ s ₁ in + let l2 ≔ s ₂ in + merge $ble (mergesort $ble l1) (mergesort $ble l2); + +assert ⊢ mergesort (≤) (3 ⸬ 1 ⸬ 4 ⸬ 1 ⸬ 5 ⸬ □) ≡ 1 ⸬ 1 ⸬ 3 ⸬ 4 ⸬ 5 ⸬ □; + +// Two-step induction and case analysis on lists, +// for the functions recursing by pairs + +opaque symbol ind_𝕃2 [a] (p : 𝕃 a → Prop) : + π (p □) → (Π x, π (p (x ⸬ □))) → + (Π x y l, π (p l) → π (p (x ⸬ y ⸬ l))) → Π l, π (p l) ≔ +begin + assume a p h0 h1 ih l; + have enough : π (p l ∧ `∀ x, p (x ⸬ l)) → π (p l) { assume h; refine ∧ₑ₁ h }; + refine enough _; + remove enough; + generalize l; + induction + { apply ∧ᵢ h0 h1 } + { assume y l ihl; + apply ∧ᵢ + { refine ∧ₑ₂ ihl y } + { assume x; refine ih x y l (∧ₑ₁ ihl) } } +end; + +opaque symbol case_𝕃2 [a] (p : 𝕃 a → Prop) : + π (p □) → (Π x, π (p (x ⸬ □))) → + (Π x y l, π (p (x ⸬ y ⸬ l))) → Π l, π (p l) ≔ +begin + assume a p h0 h1 h2; + refine ind_𝕃2 p h0 h1 _; + assume x y l ihl; refine h2 x y l +end; + +// Strong induction on the length of a list + +opaque symbol ind_𝕃_size [a] (p : 𝕃 a → Prop) : + (Π l, (Π l', π (istrue (size l' < size l)) → π (p l')) → π (p l)) → Π l, π (p l) ≔ +begin + assume a p ih; + have aux : Π n, Π l, π (istrue (size l ≤ n)) → π (p l) + { refine ind_ℕ_strong (λ n, `∀ l, istrue (size l ≤ n) ⇒ p l) _; + assume n rec l h; + refine ih l _; + assume l' h'; + refine rec (size l') (@leq_trans (size l' +1) (size l) n h' h) l' (≤_refl (size l')) }; + assume l; refine aux (size l) l (≤_refl (size l)) +end; + +// split preserves size and multiplicities + +opaque symbol size_split [a] (l : 𝕃 a) : + π (size ((split l)₁) + size ((split l)₂) = size l) ≔ +begin + assume a; + refine ind_𝕃2 (λ l, size ((split l)₁) + size ((split l)₂) = size l) _ _ _ + { reflexivity } + { assume x; reflexivity } + { assume x y l ih; simplify; rewrite addnS; rewrite ih; reflexivity } +end; + +opaque symbol count_split [a] p (l : 𝕃 a) : + π (count p ((split l)₁) + count p ((split l)₂) = count p l) ≔ +begin + assume a p; + refine ind_𝕃2 (λ l, count p ((split l)₁) + count p ((split l)₂) = count p l) _ _ _ + { reflexivity } + { assume x; simplify; rewrite addn0; reflexivity } + { assume x y l ih; simplify; + refine ∨ₑ (case_𝔹 (p x)) _ _ + { assume hx; rewrite hx; simplify; + refine ∨ₑ (case_𝔹 (p y)) _ _ + { assume hy; rewrite hy; simplify; rewrite addnS; rewrite ih; reflexivity } + { assume hy; rewrite hy; simplify; rewrite ih; reflexivity } } + { assume hx; rewrite hx; simplify; + refine ∨ₑ (case_𝔹 (p y)) _ _ + { assume hy; rewrite hy; simplify; rewrite addnS; rewrite ih; reflexivity } + { assume hy; rewrite hy; simplify; rewrite ih; reflexivity } } } +end; + +// Each half returned by split is no longer than the list + +opaque symbol size_split1 [a] (l : 𝕃 a) : π (istrue (size ((split l)₁) ≤ size l)) ≔ +begin + assume a l; rewrite left size_split l; + refine leq_addr (size ((split l)₂)) (size ((split l)₁)) +end; + +opaque symbol size_split2 [a] (l : 𝕃 a) : π (istrue (size ((split l)₂) ≤ size l)) ≔ +begin + assume a l; rewrite left size_split l; + refine leq_addl (size ((split l)₁)) (size ((split l)₂)) +end; + +// merge preserves size and multiplicities + +opaque symbol size_merge [a] (ble : τ a → τ a → 𝔹) l1 l2 : + π (size (merge ble l1 l2) = size l1 + size l2) ≔ +begin + assume a ble; + induction + { assume l2; reflexivity } + { assume x l1 ih1; + induction + { simplify; rewrite addn0; reflexivity } + { assume y l2 ih2; + refine ∨ₑ (case_𝔹 (ble x y)) _ _ + { assume h; simplify; rewrite h; simplify; + rewrite ih1 (y ⸬ l2); reflexivity } + { assume h; simplify; rewrite h; simplify; + rewrite ih2; rewrite addnS; reflexivity } } } +end; + +opaque symbol count_merge [a] p (ble : τ a → τ a → 𝔹) l1 l2 : + π (count p (merge ble l1 l2) = count p l1 + count p l2) ≔ +begin + assume a p ble; + induction + { assume l2; reflexivity } + { assume x l1 ih1; + induction + { simplify; rewrite addn0; reflexivity } + { assume y l2 ih2; + refine ∨ₑ (case_𝔹 (ble x y)) _ _ + { assume h; simplify; rewrite h; simplify; + rewrite ih1 (y ⸬ l2); + refine ∨ₑ (case_𝔹 (p x)) _ _ + { assume hx; rewrite hx; simplify; reflexivity } + { assume hx; rewrite hx; simplify; reflexivity } } + { assume h; simplify; rewrite h; simplify; + rewrite ih2; + refine ∨ₑ (case_𝔹 (p y)) _ _ + { assume hy; rewrite hy; simplify; rewrite addnS; reflexivity } + { assume hy; rewrite hy; simplify; reflexivity } } } } +end; + +// mergesort preserves size and multiplicities: its result is a permutation + +opaque symbol size_mergesort [a] (ble : τ a → τ a → 𝔹) (l : 𝕃 a) : + π (size (mergesort ble l) = size l) ≔ +begin + assume a ble; + refine ind_𝕃_size (λ l, size (mergesort ble l) = size l) _; + refine case_𝕃2 + (λ l, (`∀ l' : τ (list a), istrue (size l' < size l) + ⇒ size (mergesort ble l') = size l') + ⇒ size (mergesort ble l) = size l) _ _ _ + { assume rec; reflexivity } + { assume x rec; reflexivity } + { assume x y l rec; simplify; + rewrite size_merge; + rewrite rec (x ⸬ ((split l)₁)) (size_split1 l); + rewrite rec (y ⸬ ((split l)₂)) (size_split2 l); + simplify; rewrite addnS; rewrite size_split; reflexivity } +end; + +opaque symbol count_mergesort [a] p (ble : τ a → τ a → 𝔹) (l : 𝕃 a) : + π (count p (mergesort ble l) = count p l) ≔ +begin + assume a p ble; + refine ind_𝕃_size (λ l, count p (mergesort ble l) = count p l) _; + refine case_𝕃2 + (λ l, (`∀ l' : τ (list a), istrue (size l' < size l) + ⇒ count p (mergesort ble l') = count p l') + ⇒ count p (mergesort ble l) = count p l) _ _ _ + { assume rec; reflexivity } + { assume x rec; reflexivity } + { assume x y l rec; simplify; + rewrite count_merge; + rewrite rec (x ⸬ ((split l)₁)) (size_split1 l); + rewrite rec (y ⸬ ((split l)₂)) (size_split2 l); + simplify; + refine ∨ₑ (case_𝔹 (p x)) _ _ + { assume hx; rewrite hx; simplify; + refine ∨ₑ (case_𝔹 (p y)) _ _ + { assume hy; rewrite hy; simplify; rewrite addnS; rewrite count_split; reflexivity } + { assume hy; rewrite hy; simplify; rewrite count_split; reflexivity } } + { assume hx; rewrite hx; simplify; + refine ∨ₑ (case_𝔹 (p y)) _ _ + { assume hy; rewrite hy; simplify; rewrite addnS; rewrite count_split; reflexivity } + { assume hy; rewrite hy; simplify; rewrite count_split; reflexivity } } } +end; + +opaque symbol all_true [a] (p : τ a → 𝔹) (l : 𝕃 a) : + (Π x, π (istrue (p x))) → π (istrue (all p l)) ≔ +begin + assume a p; + induction + { assume h; refine ⊤ᵢ } + { assume x l ih h; simplify; rewrite istrue=true (h x); simplify; refine ih h } +end; + +opaque symbol perm_eq_mergesort [a] (ble : τ a → τ a → 𝔹) (l : 𝕃 a) : + π (istrue (perm_eq (λ x y, ble x y and ble y x) (mergesort ble l) l)) ≔ +begin + assume a ble l; + refine @all_true a + (λ x, eqn (count (λ y, ble x y and ble y x) (mergesort ble l)) + (count (λ y, ble x y and ble y x) l)) + ((mergesort ble l) ++ l) _; + assume x; + rewrite count_mergesort (λ y, ble x y and ble y x) ble l; + refine eqn_refl (count (λ y, ble x y and ble y x) l) +end; diff --git a/Nat.lp b/Nat.lp index 4d23901..24e14fc 100644 --- a/Nat.lp +++ b/Nat.lp @@ -88,12 +88,71 @@ expnMn : (m1 * m2) ^ n = ... The operands of other operators are selected using the l/r suffixes. */ -require open Stdlib.Bool; +require open Stdlib.Bool Stdlib.HOL; inductive ℕ : TYPE ≔ | _0 : ℕ | +1 : ℕ → ℕ; notation +1 postfix 100; +// enable printing of natural numbers in decimal notation + +builtin "nat_zero" ≔ _0; +builtin "nat_succ" ≔ +1; + +// shortcuts + +symbol _1 ≔ _0 +1; +symbol _2 ≔ _1 +1; +symbol _3 ≔ _2 +1; +symbol _4 ≔ _3 +1; +symbol _5 ≔ _4 +1; +symbol _6 ≔ _5 +1; +symbol _7 ≔ _6 +1; +symbol _8 ≔ _7 +1; +symbol _9 ≔ _8 +1; +symbol _10 ≔ _9 +1; + +// enable parsing of natural numbers in decimal notation + +builtin "0" ≔ _0; +builtin "1" ≔ _1; +builtin "2" ≔ _2; +builtin "3" ≔ _3; +builtin "4" ≔ _4; +builtin "5" ≔ _5; +builtin "6" ≔ _6; +builtin "7" ≔ _7; +builtin "8" ≔ _8; +builtin "9" ≔ _9; +builtin "10" ≔ _10; + +// Induction principle for nats from n to n+2 +opaque symbol ind_ℕ2 : Π p: (ℕ → Prop), π (p _0) → π (p (_0 +1)) → (Π x0: ℕ, π (p x0) → π (p (x0 +1)) → π (p (x0 +1 +1))) → Π x: ℕ, π (p x) ≔ +begin + assume p h0 h1 ih x; + have enough: π (p x ∧ p (x +1)) → π (p x) { assume h; refine ∧ₑ₁ h }; + refine enough _; + remove enough; + generalize x; + induction + { apply ∧ᵢ h0 h1 } + { + assume x ihx; + apply ∧ᵢ + { refine ∧ₑ₂ ihx } + { apply ih x (∧ₑ₁ ihx) (∧ₑ₂ ihx) } + } +end; + +// Perform just a case analysis without induction hypothesis +opaque symbol case_ℕ : Π p: (ℕ → Prop), π (p _0) → (Π x: ℕ, π (p (x +1))) → Π x: ℕ, π (p x) ≔ +begin + assume p h1 h2; + induction + {refine h1} + {assume x h3;apply h2} +end; + // set code for ℕ constant symbol nat : Set; @@ -184,6 +243,8 @@ symbol + : ℕ → ℕ → ℕ; notation + infix left 20; rule _0 + $y ↪ $y with $x +1 + $y ↪ ($x + $y) +1; +builtin "+" ≔ +; + opaque symbol add0n x : π (_0 + x = x) ≔ begin assume x; reflexivity; @@ -208,6 +269,13 @@ begin { assume x' h y; simplify; rewrite h; reflexivity } end; +opaque symbol suc=+1 x : π ((x +1) = (x + _1))≔ +begin + induction + {reflexivity} + {assume n h; rewrite h; rewrite left addSn; rewrite h; reflexivity;} +end; + opaque symbol add1n n : π ((_0 +1) + n = n +1) ≔ begin assume n; reflexivity; @@ -332,20 +400,52 @@ begin } end; -opaque symbol odd≠even p q : π((p + p) +1 ≠ q + q) ≔ +symbol even: ℕ → 𝔹; +rule even _0 ↪ true +with even (_0 +1) ↪ false +with even ($x +1 +1) ↪ even $x; + +symbol odd (n: ℕ): 𝔹 ≔ not (even n); + +opaque symbol evenS n : π (even (n +1) = not (even n)) ≔ begin induction - { induction - { refine s≠0 } - { assume x h; simplify; assume i; - have j: π (_0 = (x + x) +1) { rewrite left addnS x x; apply +1_inj i }; - apply 0≠s j } - } - { assume x h; induction - { refine s≠0 } - { assume y i j; apply h y; rewrite left addnS x x; apply +1_inj; - rewrite left addnS y y; apply +1_inj j } - } + { reflexivity } + { assume n ih; simplify; rewrite ih; rewrite notK; reflexivity } +end; + +opaque symbol oddS n : π (odd (n +1) = not (odd n)) ≔ +begin + assume n; simplify; rewrite evenS; reflexivity +end; + +opaque symbol even_odd n : π (even n = not (odd n)) ≔ +begin + assume n; simplify; symmetry; apply notK +end; + +opaque symbol even_addnn n : π (even (n + n)) ≔ +begin + induction + { apply ⊤ᵢ } + { assume n ih; rewrite addnS; apply ih } +end; + +opaque symbol odd_addnnS n : π (odd ((n + n) +1)) ≔ +begin + assume n; rewrite evenS; rewrite notK; refine even_addnn n +end; + +opaque symbol odd≠even m n : π (odd m) → π (even n) → π (m ≠ n) ≔ +begin + assume m n hm hn h; + refine istrue_not hm (ind_eq h (λ z, istrue (even z)) hn) +end; + +opaque symbol addnnS≠addnn p q : π ((p + p) +1 ≠ q + q) ≔ +begin + assume p q; + refine odd≠even ((p + p) +1) (q + q) (odd_addnnS p) (even_addnn q) end; // substraction @@ -485,6 +585,8 @@ assert x y z ⊢ x + y * z ≡ x + (y * z); rule _0 * _ ↪ _0 with ($x +1) * $y ↪ $y + $x * $y; +builtin "*" ≔ *; + opaque symbol mul0n x : π (x * _0 = _0) ≔ begin induction { reflexivity } { assume x' h; apply h } @@ -524,6 +626,11 @@ begin { assume x' h y; simplify; rewrite h; rewrite addnAC; reflexivity } end; +opaque symbol muln2 n: π (n * 2 = n + n) ≔ +begin +assume n; simplify; rewrite mulnS; rewrite muln1; reflexivity +end; + opaque symbol mulnSr x y : π (x * (y +1) = x * y + x) ≔ begin induction @@ -1082,6 +1189,24 @@ begin apply @leq_trans (m1 - n1) (m2 - n1) (m2 - n2) t u; end; +opaque symbol leq_exD n m : π (n ≤ m) → π (`∃ p, n + p = m) ≔ +begin + assume n m h; + refine ∨ₑ (∧ₑ₁ (leq_eqVlt n m) h) _ _ + { assume heq; refine ∃ᵢ _0 _; simplify; rewrite addn0; refine heq } + { assume hnltm; refine ∃ᵢ (m - n) _; refine subnKC n m h }; +end; + +opaque symbol exD_leq n m : π (`∃ p, n + p = m) → π (n ≤ m) ≔ +begin + assume n m h; + refine ∃ₑ h _; + assume p h2; + remove h; + rewrite left h2; + refine leq_addr p n; +end; + // max symbol max: ℕ → ℕ → ℕ; @@ -1781,44 +1906,351 @@ begin { assume n h; rewrite factS n; apply leq_pmulr (n +1) (n !) (fact_gt0 n) } end; -// enable printing of natural numbers in decimal notation -builtin "nat_zero" ≔ _0; -builtin "nat_succ" ≔ +1; +// Division by two i.e half -// shortcuts +symbol div2 : ℕ → ℕ; +rule div2 _0 ↪ _0 +with div2 (_0 +1) ↪ _0 +with div2 (($x +1) +1) ↪ (div2 $x) +1; -symbol _1 ≔ _0 +1; -symbol _2 ≔ _1 +1; -symbol _3 ≔ _2 +1; -symbol _4 ≔ _3 +1; -symbol _5 ≔ _4 +1; -symbol _6 ≔ _5 +1; -symbol _7 ≔ _6 +1; -symbol _8 ≔ _7 +1; -symbol _9 ≔ _8 +1; -symbol _10 ≔ _9 +1; +opaque symbol mul2n n : π (2 * n = n + n) ≔ +begin + assume n; rewrite mulnC; refine muln2 n +end; -opaque symbol suc=+1 x : π ((x +1) = (x + _1))≔ +opaque symbol div2_addnn x : π (div2 (x + x) = x) ≔ begin induction - {reflexivity} - {assume n h; rewrite h; rewrite left addSn; rewrite h; reflexivity;} + {reflexivity} + { assume x ih; simplify; rewrite addnS; apply feq (+1); apply ih } end; -// enable parsing of natural numbers in decimal notation +opaque symbol div2_mul2n x : π ((div2 (2 * x)) = x) ≔ +begin + assume x; rewrite mul2n; refine div2_addnn x +end; -builtin "0" ≔ _0; -builtin "1" ≔ _1; -builtin "2" ≔ _2; -builtin "3" ≔ _3; -builtin "4" ≔ _4; -builtin "5" ≔ _5; -builtin "6" ≔ _6; -builtin "7" ≔ _7; -builtin "8" ≔ _8; -builtin "9" ≔ _9; -builtin "10" ≔ _10; +opaque symbol div2_addnnS x : π (div2 ((x + x) +1) = x) ≔ +begin + induction + {reflexivity} + { assume x ih; simplify; rewrite addnS; apply feq (+1); apply ih } +end; -builtin "+" ≔ +; -builtin "*" ≔ *; +opaque symbol div2_mul2nS n : π ( div2 ((2 * n) +1) = n) ≔ +begin + assume n; rewrite mul2n; refine div2_addnnS n +end; + +opaque symbol leq_div2 n : π (div2 (n) ≤ n) ≔ +begin + refine ind_ℕ2 (λ u, istrue (div2 u ≤ u)) _ _ _ + {apply ⊤ᵢ } + {apply ⊤ᵢ } + { + assume x; + assume ih ih2; + apply @leq_trans (div2 x) x (x +1) + {refine ih} + { + refine leqnSn x + } + } +end; + +opaque symbol leq_div2Sn n : π (div2 (n +1) ≤ n) ≔ +begin + induction + {apply ⊤ᵢ } + { assume x ih; refine leq_div2 x } +end; + +opaque symbol leq_div2_leqS a n : π (a ≤ n +1) → π (div2 a ≤ n) ≔ +begin + induction + { assume n h; apply ⊤ᵢ } + { + assume a ih n h; + apply @leq_trans (div2 (a +1)) a n (leq_div2Sn a) h + } +end; + +// div2 recovers the number from its parity + +opaque symbol even_div2 n : π (even n) → π (div2 n + div2 n = n) ≔ +begin + refine ind_ℕ2 (λ u, istrue (even u) ⇒ (div2 u + div2 u = u)) _ _ _ + { assume h; reflexivity } + { assume h; apply ⊥ₑ h } + { assume x ihx ihx1 h; simplify; rewrite addnS; rewrite ihx h; reflexivity } +end; + +opaque symbol odd_div2 n : π (odd n) → π ((div2 n + div2 n) +1 = n) ≔ +begin + refine ind_ℕ2 (λ u, istrue (odd u) ⇒ ((div2 u + div2 u) +1 = u)) _ _ _ + { assume h; apply ⊥ₑ h } + { assume h; reflexivity } + { assume x ihx ihx1 h; simplify; rewrite addnS; rewrite ihx h; reflexivity } +end; + +// Bitwise operations + +symbol double x ≔ x + x; + +// shift left +// left-shifting an natural `x` with an natural `y` is equivalent to multiplying `x` with 2 raised to power `y`. +symbol <<<: ℕ → ℕ → ℕ; notation <<< infix 30; +rule $x <<< 0 ↪ $x +with $x <<< ($n +1) ↪ double ($x <<< $n); + +symbol <<: ℕ → ℕ ≔ λ x, x <<< 1 ; notation << postfix 30; + +assert ⊢ 21 <<< 1 ≡ 42; + +// shift right +// x >>> y ↪ x / (2 ^ y) +symbol >>>: ℕ → ℕ → ℕ; notation >>> infix 30; +rule $x >>> 0 ↪ $x +with $x >>> ($n +1) ↪ div2 ($x >>> $n); + +symbol >>: ℕ → ℕ ≔ λ x, x >>> 1 ; notation >> postfix 30; + +assert ⊢ 21 >>> 2 ≡ 5; + +symbol bitwise: τ (bool ⤳ bool ⤳ bool) → ℕ → ℕ → ℕ → ℕ; +rule bitwise $op _0 _ _ ↪ _0 +with bitwise $op ($n +1) $a $b ↪ (if ($op (odd $a) (odd $b)) 1 0) + 2 * (bitwise $op $n (div2 $a) (div2 $b)); + +symbol && (a b: ℕ): ℕ ≔ bitwise (and) a a b; notation && infix 10; + +symbol ⎪⎪ (a b: ℕ): ℕ ≔ bitwise (or) (max a b) a b; notation ⎪⎪ infix 12; + +assert ⊢ 2 ⎪⎪ 8 ≡ 10; + +symbol diff (a b: ℕ): ℕ ≔ bitwise (λ b1, λ b2, b1 and (not b2)) a a b; + +// Definition lxor a b := bitwise xorb (max a b) a b. +symbol xor (a b: ℕ): ℕ ≔ bitwise (xorb) (max a b) a b; notation xor infix 10; + +symbol testbit (a n: ℕ) : 𝔹; +rule testbit $a 0 ↪ odd $a +with testbit $a ($n +1) ↪ testbit (div2 $a) $n; + +symbol testbit_0_l : Π n, π (testbit 0 n = false) ≔ +begin induction { reflexivity } { assume x ih; apply ih } end; + +symbol Odd n ≔ (`∃ k, (2 * k + 1) = n); + +symbol Odd2 : Π n, π (Odd n) → π (Odd (n + 2)); + +symbol odd_spec: Π n, π (Odd n) → π (odd n = true); + +symbol Even n ≔ (`∃ k, 2 * k = n); + +symbol even_spec: Π n, π (Even n) → π (even n = true); + +symbol odd_bitwise : Π op n a b, π (odd (bitwise op (n +1) a b) = op (odd a) (odd b)) ≔ +begin + assume op n a b; + simplify bitwise; + have case: π ( + (op (odd a) (odd b) = true) + ∨ + (op (odd a) (odd b) = false)) { apply case_𝔹 }; + apply ∨ₑ case + { + assume hl; rewrite hl; simplify if; + rewrite addnC; + apply odd_spec ((_2 * bitwise op n (div2 a) (div2 b)) + _1); + apply ∃ᵢ (bitwise op n (div2 a) (div2 b)); + reflexivity + } + { + assume hr; rewrite hr; simplify if; + simplify; rewrite addn0; + refine ∧ₑ₂ (negb_false_eq_true (even (bitwise op n (div2 a) (div2 b) + bitwise op n (div2 a) (div2 b)))) _; + apply even_spec (bitwise op n (div2 a) (div2 b) + bitwise op n (div2 a) (div2 b)); + refine ∃ᵢ (bitwise op n (div2 a) (div2 b)) (mul2n (bitwise op n (div2 a) (div2 b))) + } +end; + +symbol div2_bitwise : Π op n a b, π (div2 (bitwise op (n +1) a b) = bitwise op n (div2 a) (div2 b)) ≔ +begin + assume op n a b; + simplify bitwise; + have case: π ( + (op (odd a) (odd b) = true) + ∨ + (op (odd a) (odd b) = false)) { apply case_𝔹 }; + apply ∨ₑ case + { + assume hl; rewrite hl; simplify if; + rewrite addnC; simplify; rewrite addn1; + apply div2_mul2nS + } + { + assume hr; rewrite hr; simplify if; + apply div2_mul2n (bitwise op n (div2 a) (div2 b)) + } +end; + +symbol testbit_bitwise_1 : Π op, (Π b, π ((op false b) = false)) → + Π n m a b, π (a ≤ n) → + π (testbit (bitwise op n a b) m = op (testbit a m) (testbit b m)) +≔ begin + assume op Hop; + induction + { + assume m a b Ha; + rewrite ≤0 a Ha; + simplify; + rewrite testbit_0_l; + rewrite Hop ((testbit b m)); + reflexivity + } + { + assume n IHn; + induction + { + assume a b ha; + apply odd_bitwise op (n) a b + } + { + assume m Ihm a b ha; + simplify testbit; + rewrite div2_bitwise; + apply IHn m (div2 a) (div2 b) _; + refine leq_div2_leqS a n ha + } + } +end; + +symbol testbit_bitwise_2 : Π op, π ((op false false) = false) → + Π n m a b, π (a ≤ n) → π (b ≤ n) → + π (testbit (bitwise op n a b) m = op (testbit a m) (testbit b m)) +≔ begin + assume op Hop_spec; + induction + { + assume m a b Ha Hb; + rewrite ≤0 a Ha; + rewrite ≤0 b Hb; + simplify; + rewrite testbit_0_l; + symmetry; + apply Hop_spec + } + { + assume n IHn; + induction + { + assume a b ha hb; + apply odd_bitwise op (n) a b; + } + { + assume m Ihm a b ha hb; + simplify testbit; + rewrite div2_bitwise; + apply IHn m (div2 a) (div2 b) _ _ + { refine leq_div2_leqS a n ha } + { refine leq_div2_leqS b n hb } + } + } +end; + +symbol land_spec a b n : + π (testbit (a && b) n = (testbit a n and testbit b n)) ≔ +begin + assume a n b; + simplify; + refine testbit_bitwise_1 (and) _ a b a n (≤_refl a); + induction + {reflexivity} + {reflexivity} +end; + +symbol ldiff_spec a b n : + π (testbit (diff a b) n = (testbit a n and not (testbit b n))) ≔ +begin + assume a n b; + simplify diff; + refine testbit_bitwise_1 (λ a b, a and not b) _ a b a n (≤_refl a); + induction + {reflexivity} + {reflexivity} +end; + +symbol lor_spec a b n : + π (testbit (a ⎪⎪ b) n = (testbit a n or testbit b n)) ≔ +begin + assume a n b; + simplify; + refine testbit_bitwise_2 (or) _ (max a n) b a n _ _ + {reflexivity} + {refine leq_maxl a n } + {refine leq_maxr a n } +end; + +symbol xor_spec a b n : + π (testbit (a xor b) n = (testbit a n xorb testbit b n)) ≔ +begin + assume a n b; + simplify; + refine testbit_bitwise_2 (xorb) _ (max a n) b a n _ _ + {reflexivity} + {refine leq_maxl a n } + {refine leq_maxr a n } +end; + +opaque symbol shiftr_spec: Π a n m, π (testbit (a >>> n) m = testbit a (m + n)) ≔ +begin + assume a; + induction + { assume m; rewrite addn0; reflexivity } + { + assume n ihn m; + rewrite addnS; + refine ihn (m +1) + } +end; + +opaque symbol shiftl_spec: Π a n m, π (n ≤ m) → π (testbit (a <<< n) m = testbit a (m - n)) ≔ +begin +assume a; + induction + { assume m h; rewrite sub0n; reflexivity } + { + assume n ih; + induction + { + assume contra; + apply ⊥ₑ contra + } + { + assume m ihm h; + remove ihm; + simplify; + rewrite left (ih m h); + have g: π ((((a <<< n) + (a <<< n))) = (2 * (a <<< n))) + { symmetry; refine mul2n (a <<< n) }; + rewrite g; + rewrite div2_mul2n; + reflexivity + } + } +end; +// Strong (course-of-values) induction + +opaque symbol ind_ℕ_strong (p : ℕ → Prop) : + (Π n, (Π m, π (istrue (m < n)) → π (p m)) → π (p n)) → Π n, π (p n) ≔ +begin + assume p ih n; + have aux : Π k, Π m, π (istrue (m ≤ k)) → π (p m) + { induction + { assume m h; rewrite ≤0 m h; refine ih _0 _; + assume m' h'; apply ⊥ₑ; refine ltn0 m' h' } + { assume k rec m h; refine ih m _; + assume m' h'; refine rec m' (@leq_trans (m' +1) m (k +1) h' h) } }; + refine aux n n (≤_refl n) +end; diff --git a/Pos.lp b/Pos.lp index 2a60405..b521c3e 100644 --- a/Pos.lp +++ b/Pos.lp @@ -153,7 +153,7 @@ begin { simplify; assume y i j; apply ⊥ₑ; have H: π ((((val x + (val x + 0)) +1) = (val y + (val y + 0))) ⇒ (((val x + val x) +1) = (val y + val y))) {rewrite addn0; rewrite addn0; assume h0; refine h0}; - apply odd≠even (val x) (val y) (H j) } + apply addnnS≠addnn (val x) (val y) (H j) } { simplify; assume i; apply ⊥ₑ; apply 2*val≠0 x; apply +1_inj; have H: π ((((val x + (val x + 0)) +1) = 1) ⇒ (((val x + val x) +1) = 1)) {rewrite addn0; assume h0; refine h0}; @@ -163,12 +163,12 @@ begin { simplify; assume y i j; apply ⊥ₑ; have H: π (((val x + (val x + 0)) = ((val y + (val y + 0)) +1)) ⇒ ((val x + val x) = ((val y + val y) +1))) {rewrite addn0; rewrite addn0; assume h0; refine h0}; - apply odd≠even (val y) (val x) (eq_sym (H j)) } + apply addnnS≠addnn (val y) (val x) (eq_sym (H j)) } { simplify; assume y i j; apply feq O; apply h; apply 2*_inj; have H: π (((val x + (val x + 0)) = (val y + (val y + 0))) ⇒ ((val x + val x) = (val y + val y))) {rewrite addn0; rewrite addn0; assume h0; refine h0}; apply (H j) } - { assume i; apply ⊥ₑ; apply odd≠even 0 (val x); symmetry; simplify; + { assume i; apply ⊥ₑ; apply addnnS≠addnn 0 (val x); symmetry; simplify; have H: π ((val (O x) = val H) ⇒ ((val x + val x) = 1)) {simplify val; simplify *; simplify *; simplify *; rewrite addn0; assume h0; refine h0}; apply (H i) @@ -180,7 +180,7 @@ begin have H: π ((1 = ((val x + (val x + 0)) +1)) ⇒ (1 = ((val x + val x) +1))) {rewrite addn0; assume h0; refine h0}; apply (H i) } - { simplify; assume x h i; apply ⊥ₑ; apply odd≠even 0 (val x); simplify; + { simplify; assume x h i; apply ⊥ₑ; apply addnnS≠addnn 0 (val x); simplify; have H: π ((1 = (val x + (val x + 0))) ⇒ (1 = (val x + val x))) {rewrite addn0; assume h0; refine h0}; apply (H i) } @@ -626,7 +626,125 @@ symbol mul : ℙ → ℙ → ℙ; rule mul (I $x) $y ↪ add $y (O (mul $x $y)) with mul (O $x) $y ↪ O (mul $x $y) -with mul H $y ↪ $y; +with mul H $y ↪ $y +with mul $y H ↪ $y; + +// Right reduction properties for multiplication + +opaque symbol mul_O_right p q : π (mul p (O q) = O (mul p q)) ≔ +begin + induction + { assume p prec q; simplify; rewrite prec; refine feq O _; reflexivity } + { assume p prec q; simplify; rewrite prec; refine feq O _; reflexivity } + { reflexivity } +end; + +opaque symbol mul_I_right p q : π (mul p (I q) = add p (O (mul p q))) ≔ +begin + induction + { assume p prec q; simplify; refine feq I _; + rewrite prec; rewrite left add_assoc; rewrite add_com q p; + rewrite left add_assoc; reflexivity } + { assume p prec q; simplify; refine feq O _; rewrite prec; reflexivity } + { reflexivity } +end; + +// Commutativity of multiplication + +opaque symbol mul_com x y : π (mul x y = mul y x) ≔ +begin + induction + { assume x xrec y; rewrite mul_I_right; simplify; rewrite xrec y; reflexivity } + { assume x xrec y; rewrite mul_O_right; simplify; rewrite xrec y; reflexivity } + { assume y; reflexivity } +end; + +// Interaction of multiplication with succ + +opaque symbol addnn n : π (add n n = O n) ≔ +begin + induction + { assume n nrec; simplify; rewrite left succ_add n n; rewrite nrec; reflexivity } + { assume n nrec; simplify; rewrite nrec; reflexivity } + { reflexivity } +end; + +opaque symbol mul_succ n m : π (mul (succ n) m = add (mul n m) m) ≔ +begin + induction + { assume n nrec m; symmetry; simplify; + rewrite nrec; + rewrite left addnn; + rewrite left addnn; + rewrite add_com (mul n m) m; + rewrite .[in x in _ = x] add_assoc; + rewrite .[in x in _ = x] add_com; + rewrite left add_assoc m (mul n m) (mul n m); + rewrite .[in x in x = _] add_com m (mul n m); + rewrite add_assoc (mul n m) m (mul n m); + reflexivity } + { assume n nrec m; symmetry; simplify; rewrite add_com; reflexivity } + { assume m; symmetry; simplify; apply addnn } +end; + +opaque symbol mul_succ_right n m : π (mul n (succ m) = add (mul n m) n) ≔ +begin + assume n m; + symmetry; + rewrite mul_com n (succ m); + rewrite mul_succ m n; + rewrite mul_com n m; + reflexivity +end; + +// Distributivity of multiplication over addition + +opaque symbol mul_distr_l a x y : π (mul a (add x y) = add (mul a x) (mul a y)) ≔ +begin + refine ind_ℙeano (λ a, `∀ x, `∀ y, mul a (add x y) = add (mul a x) (mul a y)) _ _ + // case H + { reflexivity } + // case succ + { assume a arec x y; + rewrite mul_succ; + rewrite (arec x y); + rewrite mul_succ; + rewrite mul_succ; + rewrite add_assoc; + rewrite add_com; + rewrite add_com x y; + rewrite left add_assoc; + rewrite add_assoc; + rewrite add_com; + rewrite add_com x (mul a x); + reflexivity } +end; + +opaque symbol mul_distr_r a x y : π (mul (add x y) a = add (mul x a) (mul y a)) ≔ +begin + assume a x y; + rewrite mul_com; + rewrite mul_com x a; + rewrite mul_com y a; + refine mul_distr_l a x y +end; + +// Associativity of multiplication + +opaque symbol mul_assoc x y z : π (mul (mul x y) z = mul x (mul y z)) ≔ +begin + assume x y; + refine ind_ℙeano (λ z, mul (mul x y) z = mul x (mul y z)) _ _ + // case H + { reflexivity } + // case succ + { assume z zrec; + rewrite mul_succ_right (mul x y) z; + rewrite mul_succ_right y z; + rewrite mul_distr_l; + rewrite zrec; + reflexivity } +end; // enable printing of positive numbers in decimal notation diff --git a/Prod.lp b/Prod.lp index b97126b..7a8873c 100644 --- a/Prod.lp +++ b/Prod.lp @@ -1,6 +1,6 @@ // Cartesian product -require open Stdlib.Set; +require open Stdlib.Prop Stdlib.Set Stdlib.HOL Stdlib.Eq Stdlib.FOL; constant symbol × : Set → Set → Set; notation × infix right 10; // \times @@ -18,3 +18,285 @@ rule ($x ‚ _)₁ ↪ $x; symbol ₂ [a b] : τ(a × b) → τ b; notation ₂ postfix 10; rule (_ ‚ $x)₂ ↪ $x; + +// Surjective pairing. `×` has no interpretation rule for `τ`, so it is opaque +// and η cannot be obtained by case analysis: we assume it. + +symbol ×_η [a b] (x: τ (a × b)) : π ((x ₁) ‚ (x ₂) = x); + +opaque symbol eq_₁ [a b] (x y: τ (a × b)) : π (x = y) → π ((x ₁) = (y ₁)) ≔ +begin assume a b x y h; refine feq (λ z, z ₁) h end; + +opaque symbol eq_₂ [a b] (x y: τ (a × b)) : π (x = y) → π ((x ₂) = (y ₂)) ≔ +begin assume a b x y h; refine feq (λ z, z ₂) h end; + +opaque symbol eq_pair [a b] (x y: τ (a × b)) : + π ((x ₁) = (y ₁)) → π ((x ₂) = (y ₂)) → π (x = y) ≔ +begin + assume a b x y h1 h2; + rewrite left (×_η x); rewrite left (×_η y); + refine feq2 (λ u v, u ‚ v) h1 h2 +end; + +opaque symbol eq_×_iff [a b] (x y: τ (a × b)) : + π (x = y ⇔ (x ₁) = (y ₁) ∧ (x ₂) = (y ₂)) ≔ +begin + assume a b x y; apply ∧ᵢ + { assume h; apply ∧ᵢ { refine eq_₁ x y h } { refine eq_₂ x y h } } + { assume h; refine eq_pair x y (∧ₑ₁ h) (∧ₑ₂ h) } +end; + +opaque symbol ‚_inj₁ [a b] (x x': τ a) (y y': τ b) : + π (x ‚ y = x' ‚ y') → π (x = x') ≔ +begin assume a b x x' y y' h; refine eq_₁ (x ‚ y) (x' ‚ y') h end; + +opaque symbol ‚_inj₂ [a b] (x x': τ a) (y y': τ b) : + π (x ‚ y = x' ‚ y') → π (y = y') ≔ +begin assume a b x x' y y' h; refine eq_₂ (x ‚ y) (x' ‚ y') h end; + +symbol map_× [a b c d] (f: τ a → τ c) (g: τ b → τ d) (x: τ (a × b)) : τ (c × d) ≔ + f (x ₁) ‚ g (x ₂); + +opaque symbol map_×_id [a b] (x: τ (a × b)) : π (map_× (λ u, u) (λ v, v) x = x) ≔ +begin assume a b x; refine ×_η x end; + +opaque symbol map_×_comp [a b c d e f] + (g: τ c → τ e) (g': τ d → τ f) (h: τ a → τ c) (h': τ b → τ d) (x: τ (a × b)) : + π (map_× g g' (map_× h h' x) = map_× (λ u, g (h u)) (λ v, g' (h' v)) x) ≔ +begin assume a b c d e f g g' h h' x; reflexivity end; + +// symmetry + +symbol swap_× [a b] (x: τ (a × b)) : τ (b × a) ≔ (x ₂) ‚ (x ₁); + +opaque symbol swap_×_invol [a b] (x: τ (a × b)) : π (swap_× (swap_× x) = x) ≔ +begin assume a b x; refine ×_η x end; + +// universal property: a map into a product is a pair of maps + +symbol pairing [a b c] (f: τ (c ⤳ a)) (g: τ (c ⤳ b)) : τ (c ⤳ (a × b)) ≔ + λ z, f z ‚ g z; + +opaque symbol ₁_pairing [a b c] (f: τ (c ⤳ a)) (g: τ (c ⤳ b)) (z: τ c) : + π ((pairing f g z ₁) = f z) ≔ +begin assume a b c f g z; reflexivity end; + +opaque symbol ₂_pairing [a b c] (f: τ (c ⤳ a)) (g: τ (c ⤳ b)) (z: τ c) : + π ((pairing f g z ₂) = g z) ≔ +begin assume a b c f g z; reflexivity end; + +opaque symbol pairing_uniq [a b c] (h: τ (c ⤳ (a × b))) (z: τ c) : + π (pairing (λ u, h u ₁) (λ u, h u ₂) z = h z) ≔ +begin assume a b c h z; refine ×_η (h z) end; + + + +// Co-Cartesian product + +(a: Set) (b: Set) inductive Sum: TYPE ≔ +| inl: τ a → Sum a b +| inr: τ b → Sum a b +; + +constant symbol sum : Set → Set → Set; + +rule τ (sum $a $b) ↪ Sum $a $b; + +// Universal property: a map out of a sum is given by case analysis + +symbol sum_case [a b c] : τ (sum a b) → (τ a → τ c) → (τ b → τ c) → τ c; + +rule sum_case (inl $x) $f _ ↪ $f $x +with sum_case (inr $y) _ $g ↪ $g $y; + +opaque symbol sum_case_uniq [a b c] (h: τ (sum a b) → τ c) (s: τ (sum a b)) : + π (sum_case s (λ x, h (inl x)) (λ y, h (inr y)) = h s) ≔ +begin + assume a b c h; induction { assume x; reflexivity } { assume y; reflexivity } +end; + +opaque symbol sum_η [a b] (s: τ (sum a b)) : + π (sum_case s (λ x, inl x) (λ y, inr y) = s) ≔ +begin + assume a b; induction { assume x; reflexivity } { assume y; reflexivity } +end; + +// non confusion of constructors +symbol is_inl [a b] : τ (sum a b) → Prop; + +rule is_inl (inl _) ↪ ⊤ +with is_inl (inr _) ↪ ⊥; + +opaque symbol inr≠inl [a b] (x: τ a) (y: τ b) : π (@inr a b y ≠ inl x) ≔ +begin assume a b x y h; refine ind_eq h (λ s, is_inl s) ⊤ᵢ end; + +opaque symbol inl≠inr [a b] (x: τ a) (y: τ b) : π (@inl a b x ≠ inr y) ≔ +begin assume a b x y h; apply inr≠inl x y; symmetry; apply h end; + +symbol outl [a b] (s: τ (sum a b)) : τ a ≔ sum_case s (λ x, x) (λ _, el a); +symbol outr [a b] (s: τ (sum a b)) : τ b ≔ sum_case s (λ _, el b) (λ y, y); + +opaque symbol inl_inj [a b] (x x': τ a) : π (@inl a b x = inl x') → π (x = x') ≔ +begin assume a b x x' h; refine feq (λ s, @outl a b s) h end; + +opaque symbol inr_inj [a b] (y y': τ b) : π (@inr a b y = inr y') → π (y = y') ≔ +begin assume a b y y' h; refine feq (λ s, @outr a b s) h end; + +// induction principle with equalities + +opaque symbol case_Sum [a b] (s: τ (sum a b)) : + π ((`∃ x, s = inl x) ∨ (`∃ y, s = inr y)) ≔ +begin + assume a b; induction + { assume x; apply ∨ᵢ₁; apply ∃ᵢ x; reflexivity } + { assume y; apply ∨ᵢ₂; apply ∃ᵢ y; reflexivity } +end; + +opaque symbol ind_Sum_eq [a b] (p: τ (sum a b) → Prop) (s: τ (sum a b)) : + (Π x, π (s = inl x) → π (p s)) → (Π y, π (s = inr y) → π (p s)) → π (p s) ≔ +begin + assume a b p s hl hr; refine ∨ₑ (case_Sum s) (λ h, ∃ₑ h hl) (λ h, ∃ₑ h hr) +end; + +symbol map_sum [a b c d] (f: τ a → τ c) (g: τ b → τ d) (s: τ (sum a b)) + : τ (sum c d) ≔ sum_case s (λ x, inl (f x)) (λ y, inr (g y)); + +opaque symbol map_sum_id [a b] (s: τ (sum a b)) : + π (map_sum (λ u, u) (λ v, v) s = s) ≔ +begin assume a b s; refine sum_η s end; + +opaque symbol map_sum_comp [a b c d e f] + (g: τ c → τ e) (g': τ d → τ f) (h: τ a → τ c) (h': τ b → τ d) (s: τ (sum a b)) : + π (map_sum g g' (map_sum h h' s) = map_sum (λ u, g (h u)) (λ v, g' (h' v)) s) ≔ +begin + assume a b c d e f g g' h h'; + induction { assume x; reflexivity } { assume y; reflexivity } +end; + +symbol swap_sum [a b] (s: τ (sum a b)) : τ (sum b a) ≔ + sum_case s (λ x, inr x) (λ y, inl y); + +opaque symbol swap_sum_invol [a b] (s: τ (sum a b)) : + π (swap_sum (swap_sum s) = s) ≔ +begin + assume a b; induction { assume x; reflexivity } { assume y; reflexivity } +end; + +// Relation between the product and the coproduct +symbol dist_× [a b c] (x: τ (a × sum b c)) : τ (sum (a × b) (a × c)) ≔ + sum_case (x ₂) (λ y, inl ((x ₁) ‚ y)) (λ z, inr ((x ₁) ‚ z)); + +symbol undist_× [a b c] (s: τ (sum (a × b) (a × c))) : τ (a × sum b c) ≔ + sum_case s (λ u, (u ₁) ‚ inl (u ₂)) (λ v, (v ₁) ‚ inr (v ₂)); + +opaque symbol undist_dist_‚ [a b c] (u: τ a) (s: τ (sum b c)) : + π (undist_× (dist_× (u ‚ s)) = u ‚ s) ≔ +begin + assume a b c u; induction { assume y; reflexivity } { assume z; reflexivity } +end; + +opaque symbol undist_dist_× [a b c] (x: τ (a × sum b c)) : + π (undist_× (dist_× x) = x) ≔ +begin + assume a b c x; rewrite left (×_η x); refine undist_dist_‚ (x ₁) (x ₂) +end; + +opaque symbol dist_undist_× [a b c] (s: τ (sum (a × b) (a × c))) : + π (dist_× (undist_× s) = s) ≔ +begin + assume a b c; induction + { assume u; refine feq (λ w, @inl (a × b) (a × c) w) (×_η u) } + { assume v; refine feq (λ w, @inr (a × b) (a × c) w) (×_η v) } +end; + +symbol sum_curry [a b c] (h: τ (sum a b ⤳ c)) : τ ((a ⤳ c) × (b ⤳ c)) ≔ + (λ x, h (inl x)) ‚ (λ y, h (inr y)); + +symbol sum_uncurry [a b c] (fg: τ ((a ⤳ c) × (b ⤳ c))) : τ (sum a b ⤳ c) ≔ + λ s, sum_case s (fg ₁) (fg ₂); + +opaque symbol sum_uncurry_curry [a b c] (h: τ (sum a b ⤳ c)) (s: τ (sum a b)) : + π (sum_uncurry (sum_curry h) s = h s) ≔ +begin + assume a b c h; induction { assume x; reflexivity } { assume y; reflexivity } +end; + +opaque symbol sum_curry_uncurry₁ [a b c] (fg: τ ((a ⤳ c) × (b ⤳ c))) (x: τ a) : + π (((sum_curry (sum_uncurry fg)) ₁) x = (fg ₁) x) ≔ +begin assume a b c fg x; reflexivity end; + +opaque symbol sum_curry_uncurry₂ [a b c] (fg: τ ((a ⤳ c) × (b ⤳ c))) (y: τ b) : + π (((sum_curry (sum_uncurry fg)) ₂) y = (fg ₂) y) ≔ +begin assume a b c fg y; reflexivity end; + + + + + +// Dependent pair of an element and a proof + +[a: Set] (p: τ a → Prop) inductive Σ : TYPE ≔ + exist (x: τ a) : π (p x) → Σ p; + +symbol s₁ [a] [p] (e: @Σ a p) : τ a; +notation s₁ postfix 12; + +rule (exist $x _) s₁ ↪ $x; + +symbol s₂ [a] [p] (e: @Σ a p) : π (p (e s₁)); +notation s₂ postfix 12; + +rule (exist _ $h) s₂ ↪ $h; + +opaque symbol Σ_∃ [a] [p] (e: @Σ a p) : π (`∃ x, p x) ≔ +begin assume a p e; refine ∃ᵢ (e s₁) (e s₂) end; + +constant symbol Sigma [a] (p: τ a → Prop) : π (`∃ x, p x) → Set; + +rule τ (@Sigma $a $p _) ↪ @Σ $a $p; + +opaque symbol Σ_η [a] [p] [h] (e: τ (@Sigma a p h)) : π (exist (e s₁) (e s₂) = e) ≔ +begin assume a p h; induction; assume x hx; reflexivity end; + +opaque symbol eq_s₁ [a] [p] [h] (x y: τ (@Sigma a p h)) : π (x = y) → π (x s₁ = y s₁) ≔ +begin assume a p h x y e; refine feq (λ z, z s₁) e end; + +opaque symbol exist_inj [a] [p] [h] (x y: τ a) (hx: π (p x)) (hy: π (p y)) : + π (@= (@Sigma a p h) (exist x hx) (exist y hy)) → π (x = y) ≔ +begin assume a p h x y hx hy e; refine @eq_s₁ a p h (exist x hx) (exist y hy) e end; + + +// Dependent pair of an element and an element in Set + +[a: Set] (p: τ a → Set) inductive sigT : TYPE ≔ + exisT (x: τ a) : τ (p x) → sigT p; + +constant symbol SigmaT [a: Set] : (τ a → Set) → Set; + +rule τ (@SigmaT $a $p) ↪ @sigT $a $p; + + +symbol st₁ [a] [p] (e: @sigT a p) : τ a; +notation st₁ postfix 12; + +rule (exisT $x _) st₁ ↪ $x; + +symbol st₂ [a] [p] (e: @sigT a p) : τ (p (e st₁)); +notation st₂ postfix 12; + +rule (exisT _ $u) st₂ ↪ $u; + +opaque symbol sigT_η [a] [p] (e: @sigT a p) : π (exisT (e st₁) (e st₂) = e) ≔ +begin assume a p; induction; assume x u; reflexivity end; + +opaque symbol eq_st₁ [a] [p] (x y: @sigT a p) : π (x = y) → π (x st₁ = y st₁) ≔ +begin assume a p x y h; refine feq (λ e, e st₁) h end; + +symbol eq_exisT [a] [p] (x y: τ a) (u: τ (p x)) (v: τ (p y)) (h: π (x = y)) : + π (transport p h u = v) → π (@exisT a p x u = exisT y v); + +opaque symbol eq_exisT_refl [a] [p] (x: τ a) (u v: τ (p x)) : + π (u = v) → π (@exisT a p x u = exisT x v) ≔ +begin + assume a p x u v h; refine feq (λ w, @exisT a p x w) h +end; diff --git a/Z.lp b/Z.lp index 7d9c28f..9929066 100644 --- a/Z.lp +++ b/Z.lp @@ -15,6 +15,39 @@ constant symbol int : Set; rule τ int ↪ ℤ; +// shortcuts + +symbol _1 ≔ Zpos _1; +symbol _2 ≔ Zpos _2; +symbol _3 ≔ Zpos _3; +symbol _4 ≔ Zpos _4; +symbol _5 ≔ Zpos _5; +symbol _6 ≔ Zpos _6; +symbol _7 ≔ Zpos _7; +symbol _8 ≔ Zpos _8; +symbol _9 ≔ Zpos _9; +symbol _10 ≔ Zpos _10; + +// enable printing of integers in decimal notation + +builtin "int_zero" ≔ Z0; +builtin "int_positive" ≔ Zpos; +builtin "int_negative" ≔ Zneg; + +// enable parsing of integers in decimal notation + +builtin "0" ≔ Z0; +builtin "1" ≔ _1; +builtin "2" ≔ _2; +builtin "3" ≔ _3; +builtin "4" ≔ _4; +builtin "5" ≔ _5; +builtin "6" ≔ _6; +builtin "7" ≔ _7; +builtin "8" ≔ _8; +builtin "9" ≔ _9; +builtin "10" ≔ _10; + // boolean functions for testing head constructor symbol isZ0 : ℤ → 𝔹; @@ -52,6 +85,14 @@ begin assume x y h; refine ind_eq h (λ n, istrue(isZneg n)) ⊤ᵢ end; +// Sign + +symbol sign : ℤ → ℤ; + +rule sign Z0 ↪ Zpos H +with sign (Zpos _) ↪ Zpos H +with sign (Zneg _) ↪ Zneg H; + // Unary opposite symbol — : ℤ → ℤ; @@ -149,6 +190,8 @@ end; symbol + : ℤ → ℤ → ℤ; notation + infix right 20; +builtin "+" ≔ +; + rule Z0 + $y ↪ $y with Zpos $x + Z0 ↪ Zpos $x with Zneg $x + Z0 ↪ Zneg $x @@ -244,6 +287,8 @@ symbol - x y ≔ x + — y; notation - infix left 20; +builtin "-" ≔ —; + opaque symbol -_same z : π (z + — z = Z0) ≔ begin induction @@ -351,6 +396,238 @@ begin { assume z; simplify; rewrite add_assoc; reflexivity } } } end; +// Compatibility of equality with the addition + +opaque symbol =_compat_add x y c : π (x = y) → π (x + c = y + c) ≔ +begin + assume x y c h; rewrite h; reflexivity +end; + +opaque symbol =_sub a b : π (a - b = Z0 ⇒ a = b) ≔ +begin + assume a b h; + have g : π ((a - b) + b = b) + { simplify; refine =_compat_add (a - b) Z0 b h }; + have g2 : π (a + (b - b) = b) + { simplify; rewrite +_com b (— b); rewrite left +_assoc; refine g }; + rewrite left +Z0 a; + rewrite left -_same b; + refine g2 +end; + + + +// Multiplication + +symbol * : ℤ → ℤ → ℤ; +notation * infix right 22; + +builtin "*" ≔ *; + +rule Z0 * _ ↪ Z0 +with _ * Z0 ↪ Z0 +with Zpos $x * Zpos $y ↪ Zpos (mul $x $y) +with Zpos $x * Zneg $y ↪ Zneg (mul $x $y) +with Zneg $x * Zpos $y ↪ Zneg (mul $x $y) +with Zneg $x * Zneg $y ↪ Zpos (mul $x $y); + + +opaque symbol *_com x y : π (x * y = y * x) ≔ +begin + induction + // case Z0 + { induction { reflexivity } { reflexivity } { reflexivity } } + // case Zpos + { assume x; + induction + { reflexivity } + { assume y; simplify; rewrite mul_com; reflexivity } + { assume y; simplify; rewrite mul_com; reflexivity } } + // case Zneg + { assume x; + induction + { reflexivity } + { assume y; simplify; rewrite mul_com; reflexivity } + { assume y; simplify; rewrite mul_com; reflexivity } } +end; + +opaque symbol *_assoc x y z : π ((x * y) * z = x * (y * z)) ≔ +begin + induction + // case Z0 + { reflexivity } + // case Zpos + { assume x; + induction + { reflexivity } + { assume y; + induction + { reflexivity } + { assume z; simplify; rewrite mul_assoc; reflexivity } + { assume z; simplify; rewrite mul_assoc; reflexivity } } + { assume y; + induction + { reflexivity } + { assume z; simplify; rewrite mul_assoc; reflexivity } + { assume z; simplify; rewrite mul_assoc; reflexivity } } } + // case Zneg + { assume x; + induction + { reflexivity } + { assume y; + induction + { reflexivity } + { assume z; simplify; rewrite mul_assoc; reflexivity } + { assume z; simplify; rewrite mul_assoc; reflexivity } } + { assume y; + induction + { reflexivity } + { assume z; simplify; rewrite mul_assoc; reflexivity } + { assume z; simplify; rewrite mul_assoc; reflexivity } } } +end; + +opaque symbol *_neutral x : π (x * Zpos H = x) ≔ +begin + induction { reflexivity } { reflexivity } { reflexivity } +end; + +opaque symbol *Z0 x : π (x * Z0 = Z0) ≔ +begin + induction { reflexivity } { reflexivity } { reflexivity } +end; + +symbol neg_mul_l a b : π (— (a * b) = (— a) * b) ≔ +begin + induction + {reflexivity} + { assume a; induction { reflexivity } { reflexivity } { reflexivity } } + { assume a; induction { reflexivity } { reflexivity } { reflexivity } } +end; + +symbol neg_mul_r a b : π (— (a * b) = a * — b) ≔ +begin + induction + {reflexivity} + { assume a; induction { reflexivity } { reflexivity } { reflexivity } } + { assume a; induction { reflexivity } { reflexivity } { reflexivity } } +end; + +opaque symbol *_Zpos_succ (a : ℙ) (s : ℤ) : π (Zpos (succ a) * s = Zpos a * s + s) ≔ +begin + assume a; + induction + { reflexivity } + { assume b; simplify; rewrite mul_succ a b; reflexivity } + { assume b; simplify; rewrite mul_succ a b; reflexivity } +end; + +opaque symbol sub_add_sub (p q r s : ℙ) : + π (sub p q + sub r s = sub (add p r) (add q s)) ≔ +begin + assume p q r s; + have e : π (sub p q + (Zpos r + Zneg s) = sub (add p r) (add q s)) + { rewrite left +_assoc (sub p q) (Zpos r) (Zneg s); + rewrite sub_add_Zpos p q r; rewrite sub_add_Zneg (add p r) q s; + reflexivity }; + refine e +end; + + +opaque symbol mul_distr_sub_pos_l (a x y : ℙ) : + π (Zpos a * sub x y = sub (mul a x) (mul a y)) ≔ +begin + assume a x y; + refine ind_ℙeano (λ a, Zpos a * sub x y = sub (mul a x) (mul a y)) _ _ a + { simplify; rewrite *_com (Zpos H) (sub x y); refine *_neutral (sub x y) } + { assume b IH; + rewrite *_Zpos_succ b (sub x y); rewrite IH; + rewrite sub_add_sub (mul b x) (mul b y) x y; + rewrite left mul_succ b x; rewrite left mul_succ b y; reflexivity } +end; + +opaque symbol mul_distr_sub_neg_l (a x y : ℙ) : + π (Zneg a * sub x y = sub (mul a y) (mul a x)) ≔ +begin + assume a x y; + have e : π ((— Zpos a) * sub x y = sub (mul a y) (mul a x)) + { rewrite left neg_mul_l (Zpos a) (sub x y); + rewrite mul_distr_sub_pos_l a x y; refine sub_opp (mul a x) (mul a y) }; + refine e +end; + + +opaque symbol *_distr_l (z x y : ℤ) : π (z * (x + y) = z * x + z * y) ≔ +begin + induction + { assume x y; reflexivity } + { assume z; + induction + { reflexivity } + { assume x; + induction + { reflexivity } + { assume y; simplify; rewrite mul_distr_l; reflexivity } + { assume y; simplify; rewrite mul_distr_sub_pos_l; reflexivity } } + { assume x; + induction + { reflexivity } + { assume y; simplify; rewrite mul_distr_sub_pos_l; reflexivity } + { assume y; simplify; rewrite mul_distr_l; reflexivity } } } + { assume z; + induction + { assume x; reflexivity } + { assume x; + induction + { reflexivity } + { assume y; simplify; rewrite mul_distr_l; reflexivity } + { assume y; simplify; rewrite mul_distr_sub_neg_l; reflexivity } } + { assume x; + induction + { reflexivity } + { assume y; simplify; rewrite mul_distr_sub_neg_l; reflexivity } + { assume y; simplify; rewrite mul_distr_l; reflexivity } } } +end; + +opaque symbol *_distr_r (x y z : ℤ) : π ((x + y) * z = x * z + y * z) ≔ +begin + assume x y z; + rewrite *_com (x + y) z; rewrite *_com x z; rewrite *_com y z; + refine *_distr_l z x y +end; + +opaque symbol distr_—_*_l a b : π (— (a * b) = (— a) * b) ≔ +begin + induction + { reflexivity } + { assume a; induction { reflexivity } { reflexivity } { reflexivity } } + { assume a; induction { reflexivity } { reflexivity } { reflexivity } } +end; + +opaque symbol distr_—_*_r a b : π (— (a * b) = a * — b) ≔ +begin + induction + { reflexivity } + { assume a; induction { reflexivity } { reflexivity } { reflexivity } } + { assume a; induction { reflexivity } { reflexivity } { reflexivity } } +end; + + + +// Exponentiation + +symbol power_pos (x : ℤ) (p : ℙ) : ℤ; + +rule power_pos $x H ↪ $x +with power_pos $x (O $p) ↪ let r ≔ power_pos $x $p in r * r +with power_pos $x (I $p) ↪ let r ≔ power_pos $x $p in $x * r * r; + +symbol ^ : ℤ → ℤ → ℤ; notation ^ infix 3; + +rule _ ^ Z0 ↪ Zpos H +with $x ^ (Zpos $p) ↪ power_pos $x $p +with _ ^ (Zneg _) ↪ Z0; + + // Comparison of integers require open Stdlib.Comp; @@ -512,6 +789,28 @@ begin { assume y; simplify; rewrite ≐_pos_sub; rewrite compare_com; reflexivity } } end; +opaque symbol ≐_mul_Zpos w r : π ((w * Zpos r ≐ Z0) = (w ≐ Z0)) ≔ +begin + induction + { assume r; reflexivity } + { assume a r; reflexivity } + { assume a r; reflexivity } +end; + +opaque symbol ≐_refl x : π (x ≐ x = Eq) ≔ +begin + induction + { reflexivity } + { induction + { assume x H; refine H } + { assume x H; refine H } + { reflexivity } } + { induction + { assume x H; refine H } + { assume x H; refine H } + { reflexivity } } +end; + // Compatibility of comparison with the addition opaque symbol ≐_compat_add x y z : π ((x ≐ y) = (x + z ≐ y + z)) ≔ @@ -523,6 +822,45 @@ begin rewrite -_same z; reflexivity; end; +opaque symbol ≐_compat_mul x y r : π ((x ≐ y) = (x * Zpos r ≐ y * Zpos r)) ≔ +begin + assume x y r; + rewrite ≐_sub x y; + rewrite ≐_sub (x * Zpos r) (y * Zpos r); + rewrite distr_—_*_l y (Zpos r); + rewrite left *_distr_r x (— y) (Zpos r); + rewrite ≐_mul_Zpos (x + — y) r; + reflexivity +end; + +// Regularity of multiplication + +opaque symbol *_reg_r x y k : π (k ≠ Z0 ⇒ x * k = y * k ⇒ x = y) ≔ +begin + assume x y; + induction + // case Z0 + { assume h0 h; apply ⊥ₑ; refine h0 (eq_refl Z0) } + // case Zpos + { assume r h0 h; + refine ≐_decides x y _; + rewrite ≐_compat_mul x y r; + rewrite h; + refine ≐_refl (y * Zpos r) } + // case Zneg + { assume r h0 h; + have ex : π (x * Zpos r = — (x * Zneg r)) + { symmetry; refine distr_—_*_r x (Zneg r) }; + have ey : π (y * Zpos r = — (y * Zneg r)) + { symmetry; refine distr_—_*_r y (Zneg r) }; + have h2 : π (x * Zpos r = y * Zpos r) + { rewrite ex; rewrite ey; rewrite h; reflexivity }; + refine ≐_decides x y _; + rewrite ≐_compat_mul x y r; + rewrite h2; + refine ≐_refl (y * Zpos r) } +end; + // Directional comparison operators symbol ≤ x y ≔ ¬ (istrue(isGt(x ≐ y))); @@ -546,6 +884,31 @@ begin { refine (λ x _, x) } end; +opaque symbol <_¬_≤ x y : π (x < y ⇒ ¬ (y ≤ x)) ≔ +begin + assume x y; + simplify; + have e : π (istrue (isLt (x ≐ y)) ⇒ ¬ ¬ (istrue (isGt (y ≐ x)))) + { rewrite ≐_com y x }; + refine ind_Comp (λ c, istrue (isLt c) ⇒ ¬ (¬ (istrue (isGt (opp c))))) _ _ _ (x ≐ y) + { assume Hbot Hbotbot; refine Hbot } + { assume H H2; refine H2 H } + { assume Hbot Hbotbot; refine Hbot }; + assume H1; refine (e H1); +end; + +opaque symbol <_¬_≥ x y : π (x < y ⇒ ¬ (x ≥ y)) ≔ +begin + assume x y; + assume xLty neg_xLty; + refine neg_xLty xLty +end; + +opaque symbol >_¬_≤ x y : π (x > y ⇒ ¬ (x ≤ y)) ≔ +begin + assume x y; refine (λ x, x); +end; + // Compatibility of directional comparison operators opaque symbol ≤_compat_add x y a : π (x ≤ y ⇒ x + a ≤ y + a) ≔ @@ -592,13 +955,55 @@ begin { assume x; assume y f h; apply ⊥ₑ; refine f } end; -// Reflexivity - opaque symbol ≤_refl x : π (x ≤ x) ≔ begin assume x; refine ≤_compat_add Z0 Z0 x _; refine (λ x, x); end; +opaque symbol ≥_refl x : π (x ≥ x) ≔ +begin + assume x; simplify; assume H; + have G : π (istrue (isLt Eq)) { rewrite left ≐_refl x; refine H }; + apply ⊥ₑ G +end; + +opaque symbol ≥_¬_< x y : π (x ≥ y ⇒ ¬ (x < y)) ≔ +begin + assume x y; assume H; refine H +end; + +opaque symbol <_irrefl x : π (¬ (x < x)) ≔ +begin + assume x; + simplify <; + refine fold_⇒ _; + rewrite ≐_refl; + refine (λ x, x); +end; + +opaque symbol >_irrefl x : π (¬ (x > x)) ≔ +begin + assume x; + simplify >; + simplify ≤; + refine fold_⇒ _; + rewrite ≐_refl; + simplify; + assume contra; + apply contra; + refine (λ x, x); +end; + +opaque symbol =_≤ x y : π (x = y ⇒ x ≤ y) ≔ +begin + assume x y Heq; rewrite Heq; refine ≤_refl y +end; + +opaque symbol =_≥ x y : π (x = y ⇒ x ≥ y) ≔ +begin + assume x y Heq; rewrite Heq; refine ≥_refl y +end; + // Antisymmetry opaque symbol ≤_antisym x y : π (x ≤ y ⇒ y ≤ x ⇒ x = y) ≔ @@ -658,51 +1063,249 @@ begin refine <_compat_add Z0 (z - x) x; end; -// Multiplication +// Relating the directional comparison operators -symbol * : ℤ → ℤ → ℤ; -notation * infix right 22; +opaque symbol ≥_≤ x y : π (x ≥ y ⇔ y ≤ x) ≔ +begin + assume x y; + apply ∧ᵢ + { have e : π (¬ (istrue (isLt (x ≐ y))) ⇒ ¬ (istrue (isGt (y ≐ x)))) + { rewrite ≐_com y x; + refine ind_Comp (λ c, ¬ (istrue (isLt c)) ⇒ ¬ (istrue (isGt (opp c)))) _ _ _ (x ≐ y) + { refine (λ x, x) } + { assume H1 H2; refine H1 H2 } + { refine (λ x, x) } }; + refine e } + { have e : π (¬ (istrue (isGt (y ≐ x))) ⇒ ¬ (istrue (isLt (x ≐ y)))) + { rewrite ≐_com y x; + refine ind_Comp (λ c, ¬ (istrue (isGt (opp c))) ⇒ ¬ (istrue (isLt c))) _ _ _ (x ≐ y) + { refine (λ x, x) } + { assume H1 H2; refine H1 H2 } + { refine (λ x, x) } }; + refine e }; +end; -rule Z0 * _ ↪ Z0 -with _ * Z0 ↪ Z0 -with Zpos $x * Zpos $y ↪ Zpos (mul $x $y) -with Zpos $x * Zneg $y ↪ Zneg (mul $x $y) -with Zneg $x * Zpos $y ↪ Zneg (mul $x $y) -with Zneg $x * Zneg $y ↪ Zpos (mul $x $y); +opaque symbol <_> x y : π (x < y ⇔ y > x) ≔ +begin + assume x y; + apply ∧ᵢ + { have e : π (istrue (isLt (x ≐ y)) ⇒ ¬ ¬ istrue (isGt (y ≐ x))) + { rewrite ≐_com; + refine ind_Comp (λ c, istrue (isLt (opp c)) ⇒ ¬ (¬ (istrue (isGt c)))) _ _ _ (y ≐ x) + { assume contra; apply ⊥ₑ contra } + { assume contra; apply ⊥ₑ contra } + { assume islt ngt; refine ngt islt } }; + refine e } + { have e : π (¬ ¬ istrue (isGt (y ≐ x)) ⇒ istrue (isLt (x ≐ y))) + { rewrite ≐_com; + refine ind_Comp (λ c, ¬ (¬ (istrue (isGt (opp c)))) ⇒ istrue (isLt c)) _ _ _ (x ≐ y) + { assume H; refine H (λ x, x) } + { assume H; apply ⊤ᵢ } + { assume H; refine H (λ x, x) } }; + refine e } +end; -// shortcuts +opaque symbol >_≥ x y : π (x > y ⇒ x ≥ y) ≔ +begin + assume x y; + refine ind_Comp (λ c, ¬ (¬ (istrue (isGt c))) ⇒ ¬ istrue (isLt c)) _ _ _ (x ≐ y) + { assume H; refine (λ x, x) } + { assume H H2; refine H (λ x, x) } + { assume H; refine (λ x, x) } +end; -symbol _1 ≔ Zpos _1; -symbol _2 ≔ Zpos _2; -symbol _3 ≔ Zpos _3; -symbol _4 ≔ Zpos _4; -symbol _5 ≔ Zpos _5; -symbol _6 ≔ Zpos _6; -symbol _7 ≔ Zpos _7; -symbol _8 ≔ Zpos _8; -symbol _9 ≔ Zpos _9; -symbol _10 ≔ Zpos _10; +opaque symbol ¬_≥_< x y : π (¬ (x ≥ y) ⇒ x < y) ≔ +begin + assume x y; + simplify; + have e : π (¬ ¬ (istrue (isLt (x ≐ y))) ⇒ istrue (isLt (x ≐ y))) + { refine ind_Comp (λ c, ¬ ¬ (istrue (isLt c)) ⇒ istrue (isLt c)) _ _ _ (x ≐ y) + { assume H; refine H (λ x, x) } + { assume H; apply ⊤ᵢ } + { assume H; refine H (λ x, x) } }; + refine e +end; -// enable printing of integers in decimal notation +opaque symbol ¬_≤_> x y : π (¬ (x ≤ y) ⇒ x > y) ≔ +begin + assume x y; refine (λ x, x) +end; -builtin "int_zero" ≔ Z0; -builtin "int_positive" ≔ Zpos; -builtin "int_negative" ≔ Zneg; +// Interaction of the comparison operators with the opposite -// enable parsing of integers in decimal notation +opaque symbol ≤_opp x y : π (x ≥ y ⇔ (— x ≤ — y)) ≔ +begin + assume x y; + simplify; + rewrite ≐_opp x y; + apply ∧ᵢ + { refine ind_Comp (λ c, (istrue (isLt c) ⇒ ⊥) ⇒ (istrue (isGt (opp c)) ⇒ ⊥)) _ _ _ (x ≐ y) + { assume H; refine H } + { assume H1 H2; refine H1 H2 } + { assume H; refine H } } + { refine ind_Comp (λ c, (istrue (isGt (opp c)) ⇒ ⊥) ⇒ (istrue (isLt c) ⇒ ⊥)) _ _ _ (x ≐ y) + { assume H; refine H } + { assume H1 H2; refine H1 H2 } + { assume H; refine H } } +end; -builtin "0" ≔ Z0; -builtin "1" ≔ _1; -builtin "2" ≔ _2; -builtin "3" ≔ _3; -builtin "4" ≔ _4; -builtin "5" ≔ _5; -builtin "6" ≔ _6; -builtin "7" ≔ _7; -builtin "8" ≔ _8; -builtin "9" ≔ _9; -builtin "10" ≔ _10; +opaque symbol <_opp x y : π (x > y ⇔ (— x < — y)) ≔ +begin + assume x y; + simplify; + rewrite ≐_opp x y; + apply ∧ᵢ + { refine ind_Comp (λ c, ((istrue (isGt c) ⇒ ⊥) ⇒ ⊥) ⇒ istrue (isLt (opp c))) _ _ _ (x ≐ y) + { assume H; refine H (λ x, x) } + { assume H; refine H (λ x, x) } + { assume H; apply ⊤ᵢ } } + { refine ind_Comp (λ c, istrue (isLt (opp c)) ⇒ ((istrue (isGt c) ⇒ ⊥) ⇒ ⊥)) _ _ _ (x ≐ y) + { assume contra H; apply contra } + { assume contra H; apply contra } + { assume Hislt Hngt; refine Hngt Hislt } } +end; -builtin "+" ≔ +; -builtin "*" ≔ *; -builtin "-" ≔ —; +// Comparison with the successor + +opaque symbol <_add_Zpos x a : π (x < x + Zpos a) ≔ +begin + assume x a; + have e : π (x + 0 = x) { refine +Z0 x }; + rewrite left .[t in t < _] e; + rewrite +_com; + rewrite +_com x (Zpos a); + refine <_compat_add 0 (Zpos a) x _; + apply ⊤ᵢ +end; + +opaque symbol ≤_¬_≥_succ t s : π (t ≤ s ⇒ ¬ (t ≥ s + Zpos H)) ≔ +begin + assume t s Ht≤s; + refine <_¬_≥ t (s + Zpos H) _; + refine <_trans_2 t s (s + Zpos H) Ht≤s _; + refine <_add_Zpos s H +end; + +// Comparison of a difference with 0 + +opaque symbol ≥_sub t s : π (t ≥ s ⇒ t - s ≥ 0) ≔ +begin + assume t s H; + refine ∧ₑ₂ (≥_≤ (t - s) 0) _; + have g : π (s ≤ t) { refine ∧ₑ₁ (≥_≤ t s) H }; + have g2 : π (s + (— s) ≤ t + (— s)) { refine ≤_compat_add s t (— s) g }; + rewrite left -_same s; + refine g2 +end; + +opaque symbol sub_≥ t s : π (t - s ≥ 0 ⇒ t ≥ s) ≔ +begin + assume t s H; + refine ∧ₑ₂ (≥_≤ t s) _; + have e : π (0 ≤ t - s) { refine (∧ₑ₁ (≥_≤ (t - s) 0)) H }; + have H2 : π (0 + s ≤ (t - s) + s) { refine ≤_compat_add 0 (t - s) s e }; + have H3 : π (0 + s ≤ t) { rewrite left simpl_inv_right t s; refine H2 }; + refine H3 +end; + +opaque symbol >_sub t s : π (t > s ⇒ t - s > 0) ≔ +begin + assume t s H; + refine ∧ₑ₁ (<_> 0 (t - s)) _; + have g : π (s < t) { refine ∧ₑ₂ (<_> s t) H }; + remove H; + have g2 : π (s + (— s) < t + (— s)) { refine <_compat_add s t (— s) g }; + rewrite left -_same s; + refine g2 +end; + +opaque symbol sub_> t s : π (t - s > 0 ⇒ t > s) ≔ +begin + assume t s H; + refine ∧ₑ₁ (<_> s t) _; + have e : π (0 < t - s) { refine (∧ₑ₂ (<_> 0 (t - s))) H }; + have H2 : π (0 + s < (t - s) + s) { refine <_compat_add 0 (t - s) s e }; + have H3 : π (0 + s < t) { rewrite left simpl_inv_right t s; refine H2 }; + refine H3 +end; + +// Compatibility of comparison with the multiplication + +opaque symbol <_compat_mul x y r : π (x < y ⇔ x * Zpos r < y * Zpos r) ≔ +begin + assume x y r; simplify; rewrite ≐_compat_mul x y r; refine ⇔_refl +end; + +opaque symbol <_compat_mul_pos p : π (Z0 < p) → Π x y, π (x < y ⇔ x * p < y * p) ≔ +begin + induction + { assume h x y; refine ⊥ₑ h } + { assume r h x y; refine <_compat_mul x y r } + { assume r h x y; refine ⊥ₑ h } +end; + +opaque symbol ≤_compat_mul x y r : π (x ≤ y ⇔ x * Zpos r ≤ y * Zpos r) ≔ +begin + assume x y r; simplify; rewrite ≐_compat_mul x y r; refine ⇔_refl +end; + +opaque symbol >_compat_mul x y r : π (x > y ⇔ x * Zpos r > y * Zpos r) ≔ +begin + assume x y r; simplify; rewrite ≐_compat_mul x y r; refine ⇔_refl +end; + +opaque symbol ≥_compat_mul x y r : π (x ≥ y ⇔ x * Zpos r ≥ y * Zpos r) ≔ +begin + assume x y r; simplify; rewrite ≐_compat_mul x y r; refine ⇔_refl +end; + +opaque symbol ≐_mul_opp x y z : π ((x * — z ≐ y * — z) = opp (x * z ≐ y * z)) ≔ +begin + assume x y z; + rewrite left distr_—_*_r x z; + rewrite left distr_—_*_r y z; + refine ≐_opp (x * z) (y * z) +end; + +opaque symbol ≐_compat_mul_neg z : π (Z0 < z) → Π x y, π ((y ≐ x) = (x * — z ≐ y * — z)) ≔ +begin + induction + { assume h x y; refine ⊥ₑ h } + { assume r h x y; + have e : π ((x * — Zpos r ≐ y * — Zpos r) = opp (x * Zpos r ≐ y * Zpos r)) + { refine ≐_mul_opp x y (Zpos r) }; + rewrite e; + rewrite left ≐_compat_mul x y r; + refine ≐_com y x } + { assume r h x y; refine ⊥ₑ h } +end; + +opaque symbol <_compat_mul_neg z : π (Z0 < z) → Π x y, π (x < y ⇔ y * — z < x * — z) ≔ +begin + induction + { assume h x y; refine ⊥ₑ h } + { assume r h x y; simplify; + rewrite ≐_compat_mul_neg (Zpos r) ⊤ᵢ y x; refine ⇔_refl } + { assume r h x y; refine ⊥ₑ h } +end; + +opaque symbol ≤_compat_mul_neg z : π (Z0 < z) → Π x y, π (x ≤ y ⇔ y * — z ≤ x * — z) ≔ +begin + induction + { assume h x y; refine ⊥ₑ h } + { assume r h x y; simplify; + rewrite ≐_compat_mul_neg (Zpos r) ⊤ᵢ y x; refine ⇔_refl } + { assume r h x y; refine ⊥ₑ h } +end; + +opaque symbol *_pos x y : π (0 < x ⇒ 0 < y ⇒ 0 < x * y) ≔ +begin + induction + { assume y h1 h2; refine ⊥ₑ h1 } + { assume a; + induction + { assume h1 h2; refine ⊥ₑ h2 } + { assume b h1 h2; refine ⊤ᵢ } + { assume b h1 h2; refine ⊥ₑ h2 } } + { assume a y h1 h2; refine ⊥ₑ h1 } +end; From 3e458855c11bf7eda42c74ff69c9ad5e2d49a535 Mon Sep 17 00:00:00 2001 From: NotBad4U Date: Tue, 29 Sep 2026 14:12:14 +0200 Subject: [PATCH 02/13] Fix all comment of PR review --- Bool.lp | 84 +++++----------- CHANGES.md | 19 ++++ Coprod.lp | 128 +++++++++++++++++++++++++ CoprodExt.lp | 17 ++++ DepProd.lp | 39 ++++++++ Epsilon.lp | 11 +-- ExtraRules.lp | 1 + HOL.lp | 5 - List.lp | 154 +++++++++++++++-------------- Nat.lp | 69 ++++++------- Pos.lp | 15 ++- Prod.lp | 261 ++------------------------------------------------ ProdExt.lp | 34 +++++++ Subset.lp | 37 +++++++ Z.lp | 54 ++++++++--- 15 files changed, 472 insertions(+), 456 deletions(-) create mode 100644 Coprod.lp create mode 100644 CoprodExt.lp create mode 100644 DepProd.lp create mode 100644 ProdExt.lp create mode 100644 Subset.lp diff --git a/Bool.lp b/Bool.lp index ad48515..1c9bd24 100644 --- a/Bool.lp +++ b/Bool.lp @@ -111,11 +111,17 @@ begin { reflexivity } end; -opaque symbol negb_false_eq_true b : π (not b = false ⇔ b = true) ≔ +opaque symbol not_inj [b c] : π (not b = not c) → π (b = c) ≔ begin -induction -{simplify; apply ∧ᵢ { assume h; reflexivity } { assume h; reflexivity }} -{simplify; apply ∧ᵢ { assume h; apply ⊥ₑ (true≠false h) } { assume h; apply ⊥ₑ (false≠true h) }} + induction + { induction + { assume h; reflexivity } + { assume h; apply ⊥ₑ (false≠true h) } + } + { induction + { assume h; apply ⊥ₑ (true≠false h) } + { assume h; reflexivity } + } end; // or @@ -145,37 +151,21 @@ end; // imp -symbol imp : 𝔹 → 𝔹 → 𝔹; +symbol imp (b c : 𝔹) : 𝔹 ≔ not b or c; notation imp infix left 20; -rule true imp true ↪ true -with true imp false ↪ false -with false imp true ↪ true -with false imp false ↪ true; - opaque symbol ⇒_istrue [p q : 𝔹] : π(p imp q) → π(p ⇒ q) ≔ begin induction { induction - { - simplify; - assume h1; refine (λ x, x) - } - { - simplify; assume h1 h2; refine h1 - } + { assume h1; refine (λ x, x) } + { assume h1 h2; refine h1 } } { induction - { - simplify; - assume h1 h2; apply h1 - } - { - simplify; - assume h1; refine (λ x, x) - } + { assume h1 h2; apply h1 } + { assume h1; refine (λ x, x) } } end; @@ -305,49 +295,29 @@ symbol xorb : 𝔹 → 𝔹 → 𝔹; notation xorb infix left 22; -rule false xorb false ↪ false -with false xorb true ↪ true -with true xorb false ↪ true -with true xorb true ↪ false; +rule false xorb $b ↪ $b +with true xorb $b ↪ not $b; opaque symbol xorbᵢ₁ [p q : 𝔹] : π p → π (not q) → π (p xorb q) ≔ begin induction - { induction - { simplify; assume h i; apply i } - { simplify; assume h i; apply ⊤ᵢ } - } - { induction - { simplify; assume h i; apply ⊥ₑ h } - { simplify; assume h i; apply ⊥ₑ h } - } + { assume q h i; apply i } + { assume q h i; apply ⊥ₑ h } end; opaque symbol xorbᵢ₂ [p q : 𝔹] : π (not p) → π q → π (p xorb q) ≔ begin induction - { induction - { simplify; assume h i; apply ⊥ₑ h } - { simplify; assume h i; apply ⊥ₑ h } - } - { induction - { simplify; assume h i; apply ⊤ᵢ } - { simplify; assume h i; apply ⊥ₑ i } - } + { assume q h i; apply ⊥ₑ h } + { assume q h i; apply i } end; opaque symbol xorbₑ [p q : 𝔹] (r : 𝔹) : π (p xorb q) → (π p → π (not q) → π r) → (π (not p) → π q → π r) → π r ≔ begin induction - { induction - { simplify; assume r h h1 h2; apply ⊥ₑ h } - { simplify; assume r h h1 h2; apply h1 ⊤ᵢ ⊤ᵢ } - } - { induction - { simplify; assume r h h1 h2; apply h2 ⊤ᵢ ⊤ᵢ } - { simplify; assume r h h1 h2; apply ⊥ₑ h } - } + { assume q r h h1 h2; apply h1 ⊤ᵢ h } + { assume q r h h1 h2; apply h2 ⊤ᵢ h } end; // if-then-else @@ -358,14 +328,10 @@ rule if true $x _ ↪ $x with if false _ $y ↪ $y; opaque symbol if_true [a] (x y : τ a) : π (if true x y = x) ≔ -begin - assume a x y; reflexivity -end; +begin reflexivity end; opaque symbol if_false [a] (x y : τ a) : π (if false x y = y) ≔ -begin - assume a x y; reflexivity -end; +begin reflexivity end; opaque symbol if_same b [a] (x : τ a) : π (if b x x = x) ≔ begin diff --git a/CHANGES.md b/CHANGES.md index 975d7cf..a20c716 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -11,11 +11,30 @@ and this project adheres to [Semantic Versioning](https://semver.org/). - Univ: universe levels for Set and Prop - Quotient: quotient types - NaryFun: n-ary functions and relations +- Bool: imp, xorb, not_inj and theorems on if-then-else +- Epsilon: εₑ +- List: foldl, foldr, All, mergesort and its correctness +- Nat: parity, div2, shifts, bitwise operations and strong induction +- Pos: theorems on multiplication +- Prod: theorems on the Cartesian product +- ProdExt: extensionality of the Cartesian product +- Coprod and CoprodExt: the co-Cartesian product (disjoint sum) +- Subset: subset types +- DepProd: dependent products and transport +- Z: theorems on multiplication, power and comparison ### Changed - Changed rewrite rules to be in line with the Rocq standard library. - Moved rules not in line with Rocq to the module ExtraRules. +- Bool: imp is now defined from not and or, and xorb uses more general rules, + to be in line with Rocq. +- Nat and Z: the builtins for parsing decimal numbers are now declared + together with those for + and *. +- Pos: moved the rule `mul x H ↪ x` to ExtraRules. +- Prod: the co-Cartesian product, subset types and dependent products have + been moved to the new modules Coprod, Subset and DepProd, and the + properties requiring surjective pairing to the new module ProdExt. ## 1.4.0 (2026-07-07) diff --git a/Coprod.lp b/Coprod.lp new file mode 100644 index 0000000..4139dd6 --- /dev/null +++ b/Coprod.lp @@ -0,0 +1,128 @@ +// Co-Cartesian product (disjoint sum) + +require open Stdlib.Prod; + +(a: Set) (b: Set) inductive Sum: TYPE ≔ +| inl: τ a → Sum a b +| inr: τ b → Sum a b +; + +constant symbol sum : Set → Set → Set; + +rule τ (sum $a $b) ↪ Sum $a $b; + +// Universal property: a map out of a sum is given by case analysis + +symbol sum_case [a b c] : τ (sum a b) → (τ a → τ c) → (τ b → τ c) → τ c; + +rule sum_case (inl $x) $f _ ↪ $f $x +with sum_case (inr $y) _ $g ↪ $g $y; + +opaque symbol sum_case_uniq [a b c] (h: τ (sum a b) → τ c) (s: τ (sum a b)) : + π (sum_case s (λ x, h (inl x)) (λ y, h (inr y)) = h s) ≔ +begin + assume a b c h; induction { reflexivity } { reflexivity } +end; + +opaque symbol sum_η [a b] (s: τ (sum a b)) : + π (sum_case s (λ x, inl x) (λ y, inr y) = s) ≔ +begin + assume a b; induction { reflexivity } { reflexivity } +end; + +// non confusion of constructors +symbol is_inl [a b] : τ (sum a b) → Prop; + +rule is_inl (inl _) ↪ ⊤ +with is_inl (inr _) ↪ ⊥; + +opaque symbol inr≠inl [a b] (x: τ a) (y: τ b) : π (@inr a b y ≠ inl x) ≔ +begin assume a b x y h; refine ind_eq h (λ s, is_inl s) ⊤ᵢ end; + +opaque symbol inl≠inr [a b] (x: τ a) (y: τ b) : π (@inl a b x ≠ inr y) ≔ +begin assume a b x y h; apply inr≠inl x y; symmetry; apply h end; + +symbol outl [a b] (s: τ (sum a b)) : τ a ≔ sum_case s (λ x, x) (λ _, el a); +symbol outr [a b] (s: τ (sum a b)) : τ b ≔ sum_case s (λ _, el b) (λ y, y); + +opaque symbol inl_inj [a b] (x x': τ a) : π (@inl a b x = inl x') → π (x = x') ≔ +begin assume a b x x' h; refine feq (λ s, @outl a b s) h end; + +opaque symbol inr_inj [a b] (y y': τ b) : π (@inr a b y = inr y') → π (y = y') ≔ +begin assume a b y y' h; refine feq (λ s, @outr a b s) h end; + +// induction principle with equalities + +opaque symbol case_Sum [a b] (s: τ (sum a b)) : + π ((`∃ x, s = inl x) ∨ (`∃ y, s = inr y)) ≔ +begin + assume a b; induction + { assume x; apply ∨ᵢ₁; apply ∃ᵢ x; reflexivity } + { assume y; apply ∨ᵢ₂; apply ∃ᵢ y; reflexivity } +end; + +opaque symbol ind_Sum_eq [a b] (p: τ (sum a b) → Prop) (s: τ (sum a b)) : + (Π x, π (s = inl x) → π (p s)) → (Π y, π (s = inr y) → π (p s)) → π (p s) ≔ +begin + assume a b p s hl hr; refine ∨ₑ (case_Sum s) (λ h, ∃ₑ h hl) (λ h, ∃ₑ h hr) +end; + +symbol map_sum [a b c d] (f: τ a → τ c) (g: τ b → τ d) (s: τ (sum a b)) + : τ (sum c d) ≔ sum_case s (λ x, inl (f x)) (λ y, inr (g y)); + +opaque symbol map_sum_id [a b] (s: τ (sum a b)) : + π (map_sum (λ u, u) (λ v, v) s = s) ≔ +begin assume a b s; refine sum_η s end; + +opaque symbol map_sum_comp [a b c d e f] + (g: τ c → τ e) (g': τ d → τ f) (h: τ a → τ c) (h': τ b → τ d) (s: τ (sum a b)) : + π (map_sum g g' (map_sum h h' s) = map_sum (λ u, g (h u)) (λ v, g' (h' v)) s) ≔ +begin + assume a b c d e f g g' h h'; + induction { reflexivity } { reflexivity } +end; + +symbol swap_sum [a b] (s: τ (sum a b)) : τ (sum b a) ≔ + sum_case s (λ x, inr x) (λ y, inl y); + +opaque symbol swap_sum_invol [a b] (s: τ (sum a b)) : + π (swap_sum (swap_sum s) = s) ≔ +begin + assume a b; induction { reflexivity } { reflexivity } +end; + +// Relation between the product and the coproduct + +symbol dist_× [a b c] (x: τ (a × sum b c)) : τ (sum (a × b) (a × c)) ≔ + sum_case (x ₂) (λ y, inl ((x ₁) ‚ y)) (λ z, inr ((x ₁) ‚ z)); + +symbol undist_× [a b c] (s: τ (sum (a × b) (a × c))) : τ (a × sum b c) ≔ + sum_case s (λ u, (u ₁) ‚ inl (u ₂)) (λ v, (v ₁) ‚ inr (v ₂)); + +opaque symbol undist_dist_‚ [a b c] (u: τ a) (s: τ (sum b c)) : + π (undist_× (dist_× (u ‚ s)) = u ‚ s) ≔ +begin + assume a b c u; induction { reflexivity } { reflexivity } +end; + +// currying + +symbol sum_curry [a b c] (h: τ (sum a b ⤳ c)) : τ ((a ⤳ c) × (b ⤳ c)) ≔ + (λ x, h (inl x)) ‚ (λ y, h (inr y)); + +symbol sum_uncurry [a b c] (fg: τ ((a ⤳ c) × (b ⤳ c))) : τ (sum a b ⤳ c) ≔ + λ s, sum_case s (fg ₁) (fg ₂); + +opaque symbol sum_uncurry_curry [a b c] (h: τ (sum a b ⤳ c)) (s: τ (sum a b)) : + π (sum_uncurry (sum_curry h) s = h s) ≔ +begin + assume a b c h; induction { reflexivity } { reflexivity } +end; + +opaque symbol sum_curry_uncurry₁ [a b c] (fg: τ ((a ⤳ c) × (b ⤳ c))) (x: τ a) : + π (((sum_curry (sum_uncurry fg)) ₁) x = (fg ₁) x) ≔ +begin reflexivity end; + +opaque symbol sum_curry_uncurry₂ [a b c] (fg: τ ((a ⤳ c) × (b ⤳ c))) (y: τ b) : + π (((sum_curry (sum_uncurry fg)) ₂) y = (fg ₂) y) ≔ +begin reflexivity end; diff --git a/CoprodExt.lp b/CoprodExt.lp new file mode 100644 index 0000000..209e98f --- /dev/null +++ b/CoprodExt.lp @@ -0,0 +1,17 @@ +/* Properties of the co-Cartesian product that require the extensionality of the Cartesian product. */ + +require open Stdlib.ProdExt Stdlib.Coprod; + +opaque symbol undist_dist_× [a b c] (x: τ (a × sum b c)) : + π (undist_× (dist_× x) = x) ≔ +begin + assume a b c x; rewrite (prodExt x); refine undist_dist_‚ (x ₁) (x ₂) +end; + +opaque symbol dist_undist_× [a b c] (s: τ (sum (a × b) (a × c))) : + π (dist_× (undist_× s) = s) ≔ +begin + assume a b c; induction + { assume u; symmetry; refine feq (λ w, @inl (a × b) (a × c) w) (prodExt u) } + { assume v; symmetry; refine feq (λ w, @inr (a × b) (a × c) w) (prodExt v) } +end; diff --git a/DepProd.lp b/DepProd.lp new file mode 100644 index 0000000..5dc7591 --- /dev/null +++ b/DepProd.lp @@ -0,0 +1,39 @@ +// Dependent product: a dependent pair of an element and an element in Set + +require open Stdlib.Prop Stdlib.Set Stdlib.Eq; + + +symbol transport [a] (p: τ a → Set) [x y: τ a] : π (x = y) → τ (p x) → τ (p y); +rule transport _ (eq_refl _) $u ↪ $u; + +[a: Set] (p: τ a → Set) inductive DProd : TYPE ≔ + dpair (x: τ a) : τ (p x) → DProd p; + +constant symbol dprod [a: Set] : (τ a → Set) → Set; + +rule τ (@dprod $a $p) ↪ @DProd $a $p; + +symbol proj₁ [a] [p] (e: @DProd a p) : τ a; + +rule proj₁ (dpair $x _) ↪ $x; + +symbol proj₂ [a] [p] (e: @DProd a p) : τ (p (proj₁ e)); + +rule proj₂ (dpair _ $u) ↪ $u; + +opaque symbol DProd_η [a] [p] (e: @DProd a p) : + π (dpair (proj₁ e) (proj₂ e) = e) ≔ +begin assume a p; induction; assume x u; reflexivity end; + +opaque symbol eq_proj₁ [a] [p] (x y: @DProd a p) : + π (x = y) → π (proj₁ x = proj₁ y) ≔ +begin assume a p x y h; refine feq (λ e, proj₁ e) h end; + +symbol eq_dpair [a] [p] (x y: τ a) (u: τ (p x)) (v: τ (p y)) (h: π (x = y)) : + π (transport p h u = v) → π (@dpair a p x u = dpair y v); + +opaque symbol eq_dpair_refl [a] [p] (x: τ a) (u v: τ (p x)) : + π (u = v) → π (@dpair a p x u = dpair x v) ≔ +begin + assume a p x u v h; refine feq (λ w, @dpair a p x w) h +end; diff --git a/Epsilon.lp b/Epsilon.lp index a00783e..462536d 100644 --- a/Epsilon.lp +++ b/Epsilon.lp @@ -1,12 +1,9 @@ -require open Stdlib.FOL Stdlib.FunExt Stdlib.Impred; +require open Stdlib.FOL; symbol ε [a:Set] : (τ a → Prop) → τ a; symbol εᵢ [a:Set] (p:τ a → Prop) : π (∃ p) → π (p (ε p)); -opaque symbol εₑ [a:Set] (p:τ a → Prop) : π (p (ε p)) → π (∃ p) ≔ +opaque symbol εₑ [a:Set] (p:τ a → Prop) : π (p (ε p)) → π (`∃ x, p x) ≔ begin - assume a p h; - have e : π ((λ x, p x) = p) { refine funExt (λ x, p x) p (λ x, eq_refl (p x)) }; - rewrite left e; - refine ∃ᵢ (ε p) h -end; \ No newline at end of file + assume a p h; refine ∃ᵢ (ε p) h +end; diff --git a/ExtraRules.lp b/ExtraRules.lp index ce9aa22..0259466 100644 --- a/ExtraRules.lp +++ b/ExtraRules.lp @@ -39,6 +39,7 @@ rule P.add $x P.H ↪ P.succ $x with P.add P.H $y ↪ P.succ $y; rule P.add_carry $x P.H ↪ P.add $x (P.O P.H) with P.add_carry P.H $y ↪ P.add (P.O P.H) $y; +rule P.mul $x P.H ↪ $x; // Z diff --git a/HOL.lp b/HOL.lp index 0204d0d..156135b 100644 --- a/HOL.lp +++ b/HOL.lp @@ -18,8 +18,3 @@ rule τ ($a ⤳d λ x,$b.[x]) ↪ Π x:τ $a, τ $b.[x]; symbol ∘ [a b c] : τ (b ⤳ c) → τ (a ⤳ b) → τ a → τ c ≔ λ g f x, g (f x); notation ∘ infix 20; - -symbol transport [a] (p: τ a → Set) [x y: τ a] : π (x = y) → τ (p x) → τ (p y); - -rule @transport _ _ $x $x _ $u ↪ $u -with @transport _ (λ _, _) _ _ _ $u ↪ $u; diff --git a/List.lp b/List.lp index 757d0d8..ed69395 100644 --- a/List.lp +++ b/List.lp @@ -204,7 +204,7 @@ protected with nosimpl. An example of use can be found in fingraph theorem orbitPcycle. */ -require open Stdlib.Nat Stdlib.Prod Stdlib.HOL; +require open Stdlib.Nat Stdlib.Prod; (a:Set) inductive 𝕃:TYPE ≔ | □ : 𝕃 a // \Box @@ -1903,69 +1903,61 @@ begin refine eq_refl (x ⸬ l) } end; -// sumn - -symbol sumn : 𝕃 nat → ℕ; - -rule sumn □ ↪ 0 -with sumn ($x ⸬ $l) ↪ $x + sumn $l; - -assert ⊢ sumn (3 ⸬ 2 ⸬ 1 ⸬ □) ≡ 6; - -// prodn - -symbol prodn : 𝕃 nat → ℕ; +// foldr -rule prodn □ ↪ 1 -with prodn ($x ⸬ $l) ↪ $x * prodn $l; +symbol foldr [a b] : (τ b → τ a → τ a) → τ a → 𝕃 b → τ a; -assert ⊢ prodn (3 ⸬ 2 ⸬ 1 ⸬ □) ≡ 3 !; +rule foldr _ $acc □ ↪ $acc +with foldr $op $acc ($h ⸬ $tl) ↪ $op $h (foldr $op $acc $tl); // foldl -symbol foldl [a b] : τ (a ⤳ b ⤳ a) → τ a → 𝕃 b → τ a; +symbol foldl [a b] : (τ a → τ b → τ a) → τ a → 𝕃 b → τ a; rule foldl _ $acc □ ↪ $acc with foldl $op $acc ($h ⸬ $tl) ↪ foldl $op ($op $acc $h) $tl; -assert ⊢ sumn (3 ⸬ 2 ⸬ 1 ⸬ □) ≡ foldl (+) 0 (3 ⸬ 2 ⸬ 1 ⸬ □); +assert ⊢ foldl (+) 0 (3 ⸬ 2 ⸬ 1 ⸬ □) ≡ foldr (+) 0 (3 ⸬ 2 ⸬ 1 ⸬ □); -// foldr +// sumn -symbol foldr [a b] : τ (b ⤳ a ⤳ a) → τ a → 𝕃 b → τ a; +symbol sumn (l : 𝕃 nat) : ℕ ≔ foldr (+) 0 l; -rule foldr _ $acc □ ↪ $acc -with foldr $op $acc ($h ⸬ $tl) ↪ $op $h (foldr $op $acc $tl); +assert ⊢ sumn (3 ⸬ 2 ⸬ 1 ⸬ □) ≡ 6; + +// prodn + +symbol prodn (l : 𝕃 nat) : ℕ ≔ foldr (*) 1 l; -assert ⊢ sumn (3 ⸬ 2 ⸬ 1 ⸬ □) ≡ foldr (+) 0 (3 ⸬ 2 ⸬ 1 ⸬ □); +assert ⊢ prodn (3 ⸬ 2 ⸬ 1 ⸬ □) ≡ 3 !; // Sorting algorithm Merge Sort -symbol split [a: Set] (l : τ (list a)): τ(list a × list a); -rule split □ ↪ (□ ‚ □) -with split ($x ⸬ □) ↪ (($x ⸬ □) ‚ □) +symbol split [a: Set] (l : τ (list a)) : τ (list a × list a); + +rule split □ ↪ □ ‚ □ +with split ($x ⸬ □) ↪ ($x ⸬ □) ‚ □ with split ($x ⸬ $y ⸬ $l) ↪ - let res ≔ (split $l) in - ($x ⸬ (res ₁)) ‚ ($y ⸬ (res ₂)); + let res ≔ split $l in ($x ⸬ (res ₁)) ‚ ($y ⸬ (res ₂)); // merge and mergesort are parametrised by a boolean ordering on the elements symbol merge [a] : (τ a → τ a → 𝔹) → 𝕃 a → 𝕃 a → 𝕃 a; + rule merge _ □ $l2 ↪ $l2 with merge _ $l1 □ ↪ $l1 -with merge $ble ($a1 ⸬ $l1') ($a2 ⸬ $l2') ↪ - if ($ble $a1 $a2) - ($a1 ⸬ merge $ble $l1' ($a2 ⸬ $l2')) - ($a2 ⸬ merge $ble ($a1 ⸬ $l1') $l2'); +with merge $≤ ($a1 ⸬ $l1') ($a2 ⸬ $l2') ↪ + if ($≤ $a1 $a2) + ($a1 ⸬ merge $≤ $l1' ($a2 ⸬ $l2')) + ($a2 ⸬ merge $≤ ($a1 ⸬ $l1') $l2'); symbol mergesort [a] : (τ a → τ a → 𝔹) → 𝕃 a → 𝕃 a; + rule mergesort _ □ ↪ □ -with mergesort _ ($x ⸬ □) ↪ ($x ⸬ □) -with mergesort $ble ($x ⸬ $y ⸬ $l) ↪ - let s ≔ split ($x ⸬ $y ⸬ $l) in - let l1 ≔ s ₁ in - let l2 ≔ s ₂ in - merge $ble (mergesort $ble l1) (mergesort $ble l2); +with mergesort _ ($x ⸬ □) ↪ $x ⸬ □ +with mergesort $≤ ($x ⸬ $y ⸬ $l) ↪ + merge $≤ (mergesort $≤ ($x ⸬ ((split $l)₁))) + (mergesort $≤ ($y ⸬ ((split $l)₂))); assert ⊢ mergesort (≤) (3 ⸬ 1 ⸬ 4 ⸬ 1 ⸬ 5 ⸬ □) ≡ 1 ⸬ 1 ⸬ 3 ⸬ 4 ⸬ 5 ⸬ □; @@ -2060,34 +2052,34 @@ end; // merge preserves size and multiplicities -opaque symbol size_merge [a] (ble : τ a → τ a → 𝔹) l1 l2 : - π (size (merge ble l1 l2) = size l1 + size l2) ≔ +opaque symbol size_merge [a] (≤ : τ a → τ a → 𝔹) l1 l2 : + π (size (merge (≤) l1 l2) = size l1 + size l2) ≔ begin - assume a ble; + assume a ≤; induction { assume l2; reflexivity } { assume x l1 ih1; induction { simplify; rewrite addn0; reflexivity } { assume y l2 ih2; - refine ∨ₑ (case_𝔹 (ble x y)) _ _ + refine ∨ₑ (case_𝔹 ((≤) x y)) _ _ { assume h; simplify; rewrite h; simplify; rewrite ih1 (y ⸬ l2); reflexivity } { assume h; simplify; rewrite h; simplify; rewrite ih2; rewrite addnS; reflexivity } } } end; -opaque symbol count_merge [a] p (ble : τ a → τ a → 𝔹) l1 l2 : - π (count p (merge ble l1 l2) = count p l1 + count p l2) ≔ +opaque symbol count_merge [a] p (≤ : τ a → τ a → 𝔹) l1 l2 : + π (count p (merge (≤) l1 l2) = count p l1 + count p l2) ≔ begin - assume a p ble; + assume a p ≤; induction { assume l2; reflexivity } { assume x l1 ih1; induction { simplify; rewrite addn0; reflexivity } { assume y l2 ih2; - refine ∨ₑ (case_𝔹 (ble x y)) _ _ + refine ∨ₑ (case_𝔹 ((≤) x y)) _ _ { assume h; simplify; rewrite h; simplify; rewrite ih1 (y ⸬ l2); refine ∨ₑ (case_𝔹 (p x)) _ _ @@ -2102,17 +2094,17 @@ end; // mergesort preserves size and multiplicities: its result is a permutation -opaque symbol size_mergesort [a] (ble : τ a → τ a → 𝔹) (l : 𝕃 a) : - π (size (mergesort ble l) = size l) ≔ +opaque symbol size_mergesort [a] (≤ : τ a → τ a → 𝔹) (l : 𝕃 a) : + π (size (mergesort (≤) l) = size l) ≔ begin - assume a ble; - refine ind_𝕃_size (λ l, size (mergesort ble l) = size l) _; + assume a ≤; + refine ind_𝕃_size (λ l, size (mergesort (≤) l) = size l) _; refine case_𝕃2 (λ l, (`∀ l' : τ (list a), istrue (size l' < size l) - ⇒ size (mergesort ble l') = size l') - ⇒ size (mergesort ble l) = size l) _ _ _ - { assume rec; reflexivity } - { assume x rec; reflexivity } + ⇒ size (mergesort (≤) l') = size l') + ⇒ size (mergesort (≤) l) = size l) _ _ _ + { reflexivity } + { reflexivity } { assume x y l rec; simplify; rewrite size_merge; rewrite rec (x ⸬ ((split l)₁)) (size_split1 l); @@ -2120,17 +2112,17 @@ begin simplify; rewrite addnS; rewrite size_split; reflexivity } end; -opaque symbol count_mergesort [a] p (ble : τ a → τ a → 𝔹) (l : 𝕃 a) : - π (count p (mergesort ble l) = count p l) ≔ +opaque symbol count_mergesort [a] p (≤ : τ a → τ a → 𝔹) (l : 𝕃 a) : + π (count p (mergesort (≤) l) = count p l) ≔ begin - assume a p ble; - refine ind_𝕃_size (λ l, count p (mergesort ble l) = count p l) _; + assume a p ≤; + refine ind_𝕃_size (λ l, count p (mergesort (≤) l) = count p l) _; refine case_𝕃2 (λ l, (`∀ l' : τ (list a), istrue (size l' < size l) - ⇒ count p (mergesort ble l') = count p l') - ⇒ count p (mergesort ble l) = count p l) _ _ _ - { assume rec; reflexivity } - { assume x rec; reflexivity } + ⇒ count p (mergesort (≤) l') = count p l') + ⇒ count p (mergesort (≤) l) = count p l) _ _ _ + { reflexivity } + { reflexivity } { assume x y l rec; simplify; rewrite count_merge; rewrite rec (x ⸬ ((split l)₁)) (size_split1 l); @@ -2147,24 +2139,28 @@ begin { assume hy; rewrite hy; simplify; rewrite count_split; reflexivity } } } end; -opaque symbol all_true [a] (p : τ a → 𝔹) (l : 𝕃 a) : - (Π x, π (istrue (p x))) → π (istrue (all p l)) ≔ +opaque symbol all_true [a] (≤ : τ a → τ a → 𝔹) (≤_refl : Π x, π (≤ x x)) + (p : τ a → 𝔹) (l : 𝕃 a) : + (Π x, π (∈ (≤) x l) → π (p x)) → π (all p l) ≔ begin - assume a p; + assume a ≤ ≤_refl p; induction { assume h; refine ⊤ᵢ } - { assume x l ih h; simplify; rewrite istrue=true (h x); simplify; refine ih h } -end; - -opaque symbol perm_eq_mergesort [a] (ble : τ a → τ a → 𝔹) (l : 𝕃 a) : - π (istrue (perm_eq (λ x y, ble x y and ble y x) (mergesort ble l) l)) ≔ -begin - assume a ble l; - refine @all_true a - (λ x, eqn (count (λ y, ble x y and ble y x) (mergesort ble l)) - (count (λ y, ble x y and ble y x) l)) - ((mergesort ble l) ++ l) _; - assume x; - rewrite count_mergesort (λ y, ble x y and ble y x) ble l; - refine eqn_refl (count (λ y, ble x y and ble y x) l) + { assume y l ih h; + have hy : π (p y) { refine h y (orᵢ₁ (∈ (≤) y l) (≤_refl y)) }; + simplify; rewrite istrue=true hy; simplify; + refine ih (λ x hx, h x (orᵢ₂ ((≤) x y) hx)) } +end; + +opaque symbol perm_eq_mergesort [a] (≤ : τ a → τ a → 𝔹) (l : 𝕃 a) : + π (perm_eq (λ x y, (≤) x y and (≤) y x) (mergesort (≤) l) l) ≔ +begin + assume a ≤ l; + refine all_true (λ _ _, true) (λ _, ⊤ᵢ) + (λ x, eqn (count (λ y, ≤ x y and ≤ y x) (mergesort ≤ l)) + (count (λ y, ≤ x y and ≤ y x) l)) + ((mergesort ≤ l) ++ l) _; + assume x hx; + rewrite count_mergesort (λ y, (≤) x y and (≤) y x) (≤) l; + refine eqn_refl (count (λ y, (≤) x y and (≤) y x) l) end; diff --git a/Nat.lp b/Nat.lp index 24e14fc..59a160c 100644 --- a/Nat.lp +++ b/Nat.lp @@ -88,7 +88,7 @@ expnMn : (m1 * m2) ^ n = ... The operands of other operators are selected using the l/r suffixes. */ -require open Stdlib.Bool Stdlib.HOL; +require open Stdlib.Bool; inductive ℕ : TYPE ≔ | _0 : ℕ @@ -112,22 +112,8 @@ symbol _8 ≔ _7 +1; symbol _9 ≔ _8 +1; symbol _10 ≔ _9 +1; -// enable parsing of natural numbers in decimal notation - -builtin "0" ≔ _0; -builtin "1" ≔ _1; -builtin "2" ≔ _2; -builtin "3" ≔ _3; -builtin "4" ≔ _4; -builtin "5" ≔ _5; -builtin "6" ≔ _6; -builtin "7" ≔ _7; -builtin "8" ≔ _8; -builtin "9" ≔ _9; -builtin "10" ≔ _10; - // Induction principle for nats from n to n+2 -opaque symbol ind_ℕ2 : Π p: (ℕ → Prop), π (p _0) → π (p (_0 +1)) → (Π x0: ℕ, π (p x0) → π (p (x0 +1)) → π (p (x0 +1 +1))) → Π x: ℕ, π (p x) ≔ +opaque symbol ind_ℕ2 (p : ℕ → Prop) : π (p _0) → π (p (_0 +1)) → (Π x0: ℕ, π (p x0) → π (p (x0 +1)) → π (p (x0 +1 +1))) → Π x: ℕ, π (p x) ≔ begin assume p h0 h1 ih x; have enough: π (p x ∧ p (x +1)) → π (p x) { assume h; refine ∧ₑ₁ h }; @@ -145,7 +131,7 @@ begin end; // Perform just a case analysis without induction hypothesis -opaque symbol case_ℕ : Π p: (ℕ → Prop), π (p _0) → (Π x: ℕ, π (p (x +1))) → Π x: ℕ, π (p x) ≔ +opaque symbol case_ℕ (p : ℕ → Prop) : π (p _0) → (Π x: ℕ, π (p (x +1))) → Π x: ℕ, π (p x) ≔ begin assume p h1 h2; induction @@ -587,6 +573,20 @@ with ($x +1) * $y ↪ $y + $x * $y; builtin "*" ≔ *; +// enable parsing of natural numbers in decimal notation + +builtin "0" ≔ _0; +builtin "1" ≔ _1; +builtin "2" ≔ _2; +builtin "3" ≔ _3; +builtin "4" ≔ _4; +builtin "5" ≔ _5; +builtin "6" ≔ _6; +builtin "7" ≔ _7; +builtin "8" ≔ _8; +builtin "9" ≔ _9; +builtin "10" ≔ _10; + opaque symbol mul0n x : π (x * _0 = _0) ≔ begin induction { reflexivity } { assume x' h; apply h } @@ -2018,9 +2018,11 @@ symbol >>: ℕ → ℕ ≔ λ x, x >>> 1 ; notation >> postfix 30; assert ⊢ 21 >>> 2 ≡ 5; -symbol bitwise: τ (bool ⤳ bool ⤳ bool) → ℕ → ℕ → ℕ → ℕ; -rule bitwise $op _0 _ _ ↪ _0 -with bitwise $op ($n +1) $a $b ↪ (if ($op (odd $a) (odd $b)) 1 0) + 2 * (bitwise $op $n (div2 $a) (div2 $b)); +symbol bitwise : (𝔹 → 𝔹 → 𝔹) → ℕ → ℕ → ℕ → ℕ; + +rule bitwise _ _0 _ _ ↪ _0 +with bitwise $op ($n +1) $a $b ↪ + (if ($op (odd $a) (odd $b)) 1 0) + 2 * bitwise $op $n (div2 $a) (div2 $b); symbol && (a b: ℕ): ℕ ≔ bitwise (and) a a b; notation && infix 10; @@ -2037,20 +2039,20 @@ symbol testbit (a n: ℕ) : 𝔹; rule testbit $a 0 ↪ odd $a with testbit $a ($n +1) ↪ testbit (div2 $a) $n; -symbol testbit_0_l : Π n, π (testbit 0 n = false) ≔ +symbol testbit_0_l n : π (testbit 0 n = false) ≔ begin induction { reflexivity } { assume x ih; apply ih } end; symbol Odd n ≔ (`∃ k, (2 * k + 1) = n); -symbol Odd2 : Π n, π (Odd n) → π (Odd (n + 2)); +symbol Odd2 n : π (Odd n) → π (Odd (n + 2)); -symbol odd_spec: Π n, π (Odd n) → π (odd n = true); +symbol odd_spec n : π (Odd n) → π (odd n = true); symbol Even n ≔ (`∃ k, 2 * k = n); -symbol even_spec: Π n, π (Even n) → π (even n = true); +symbol even_spec n : π (Even n) → π (even n = true); -symbol odd_bitwise : Π op n a b, π (odd (bitwise op (n +1) a b) = op (odd a) (odd b)) ≔ +symbol odd_bitwise op n a b : π (odd (bitwise op (n +1) a b) = op (odd a) (odd b)) ≔ begin assume op n a b; simplify bitwise; @@ -2069,13 +2071,14 @@ begin { assume hr; rewrite hr; simplify if; simplify; rewrite addn0; - refine ∧ₑ₂ (negb_false_eq_true (even (bitwise op n (div2 a) (div2 b) + bitwise op n (div2 a) (div2 b)))) _; + refine @feq bool bool not (even (bitwise op n (div2 a) (div2 b) + bitwise op n (div2 a) (div2 b))) true _; apply even_spec (bitwise op n (div2 a) (div2 b) + bitwise op n (div2 a) (div2 b)); refine ∃ᵢ (bitwise op n (div2 a) (div2 b)) (mul2n (bitwise op n (div2 a) (div2 b))) } end; -symbol div2_bitwise : Π op n a b, π (div2 (bitwise op (n +1) a b) = bitwise op n (div2 a) (div2 b)) ≔ +symbol div2_bitwise op n a b : + π (div2 (bitwise op (n +1) a b) = bitwise op n (div2 a) (div2 b)) ≔ begin assume op n a b; simplify bitwise; @@ -2095,8 +2098,8 @@ begin } end; -symbol testbit_bitwise_1 : Π op, (Π b, π ((op false b) = false)) → - Π n m a b, π (a ≤ n) → +symbol testbit_bitwise_1 op (hop : Π b, π (op false b = false)) n m a b : + π (a ≤ n) → π (testbit (bitwise op n a b) m = op (testbit a m) (testbit b m)) ≔ begin assume op Hop; @@ -2126,8 +2129,8 @@ symbol testbit_bitwise_1 : Π op, (Π b, π ((op false b) = false)) → } end; -symbol testbit_bitwise_2 : Π op, π ((op false false) = false) → - Π n m a b, π (a ≤ n) → π (b ≤ n) → +symbol testbit_bitwise_2 op (hop : π (op false false = false)) n m a b : + π (a ≤ n) → π (b ≤ n) → π (testbit (bitwise op n a b) m = op (testbit a m) (testbit b m)) ≔ begin assume op Hop_spec; @@ -2203,7 +2206,7 @@ begin {refine leq_maxr a n } end; -opaque symbol shiftr_spec: Π a n m, π (testbit (a >>> n) m = testbit a (m + n)) ≔ +opaque symbol shiftr_spec a n m : π (testbit (a >>> n) m = testbit a (m + n)) ≔ begin assume a; induction @@ -2215,7 +2218,7 @@ begin } end; -opaque symbol shiftl_spec: Π a n m, π (n ≤ m) → π (testbit (a <<< n) m = testbit a (m - n)) ≔ +opaque symbol shiftl_spec a n m : π (n ≤ m) → π (testbit (a <<< n) m = testbit a (m - n)) ≔ begin assume a; induction diff --git a/Pos.lp b/Pos.lp index b521c3e..a7b4427 100644 --- a/Pos.lp +++ b/Pos.lp @@ -626,8 +626,7 @@ symbol mul : ℙ → ℙ → ℙ; rule mul (I $x) $y ↪ add $y (O (mul $x $y)) with mul (O $x) $y ↪ O (mul $x $y) -with mul H $y ↪ $y -with mul $y H ↪ $y; +with mul H $y ↪ $y; // Right reduction properties for multiplication @@ -649,6 +648,14 @@ begin { reflexivity } end; +opaque symbol mul_H_right p : π (mul p H = p) ≔ +begin + induction + { assume p prec; simplify; rewrite prec; reflexivity } + { assume p prec; simplify; rewrite prec; reflexivity } + { reflexivity } +end; + // Commutativity of multiplication opaque symbol mul_com x y : π (mul x y = mul y x) ≔ @@ -656,7 +663,7 @@ begin induction { assume x xrec y; rewrite mul_I_right; simplify; rewrite xrec y; reflexivity } { assume x xrec y; rewrite mul_O_right; simplify; rewrite xrec y; reflexivity } - { assume y; reflexivity } + { assume y; rewrite mul_H_right; reflexivity } end; // Interaction of multiplication with succ @@ -736,7 +743,7 @@ begin assume x y; refine ind_ℙeano (λ z, mul (mul x y) z = mul x (mul y z)) _ _ // case H - { reflexivity } + { simplify; rewrite mul_H_right; rewrite mul_H_right; reflexivity } // case succ { assume z zrec; rewrite mul_succ_right (mul x y) z; diff --git a/Prod.lp b/Prod.lp index 7a8873c..94592f4 100644 --- a/Prod.lp +++ b/Prod.lp @@ -1,6 +1,6 @@ // Cartesian product -require open Stdlib.Prop Stdlib.Set Stdlib.HOL Stdlib.Eq Stdlib.FOL; +require open Stdlib.Prop Stdlib.Set Stdlib.Eq; constant symbol × : Set → Set → Set; notation × infix right 10; // \times @@ -19,33 +19,12 @@ symbol ₂ [a b] : τ(a × b) → τ b; notation ₂ postfix 10; rule (_ ‚ $x)₂ ↪ $x; -// Surjective pairing. `×` has no interpretation rule for `τ`, so it is opaque -// and η cannot be obtained by case analysis: we assume it. - -symbol ×_η [a b] (x: τ (a × b)) : π ((x ₁) ‚ (x ₂) = x); - opaque symbol eq_₁ [a b] (x y: τ (a × b)) : π (x = y) → π ((x ₁) = (y ₁)) ≔ begin assume a b x y h; refine feq (λ z, z ₁) h end; opaque symbol eq_₂ [a b] (x y: τ (a × b)) : π (x = y) → π ((x ₂) = (y ₂)) ≔ begin assume a b x y h; refine feq (λ z, z ₂) h end; -opaque symbol eq_pair [a b] (x y: τ (a × b)) : - π ((x ₁) = (y ₁)) → π ((x ₂) = (y ₂)) → π (x = y) ≔ -begin - assume a b x y h1 h2; - rewrite left (×_η x); rewrite left (×_η y); - refine feq2 (λ u v, u ‚ v) h1 h2 -end; - -opaque symbol eq_×_iff [a b] (x y: τ (a × b)) : - π (x = y ⇔ (x ₁) = (y ₁) ∧ (x ₂) = (y ₂)) ≔ -begin - assume a b x y; apply ∧ᵢ - { assume h; apply ∧ᵢ { refine eq_₁ x y h } { refine eq_₂ x y h } } - { assume h; refine eq_pair x y (∧ₑ₁ h) (∧ₑ₂ h) } -end; - opaque symbol ‚_inj₁ [a b] (x x': τ a) (y y': τ b) : π (x ‚ y = x' ‚ y') → π (x = x') ≔ begin assume a b x x' y y' h; refine eq_₁ (x ‚ y) (x' ‚ y') h end; @@ -57,246 +36,20 @@ begin assume a b x x' y y' h; refine eq_₂ (x ‚ y) (x' ‚ y') h end; symbol map_× [a b c d] (f: τ a → τ c) (g: τ b → τ d) (x: τ (a × b)) : τ (c × d) ≔ f (x ₁) ‚ g (x ₂); -opaque symbol map_×_id [a b] (x: τ (a × b)) : π (map_× (λ u, u) (λ v, v) x = x) ≔ -begin assume a b x; refine ×_η x end; - opaque symbol map_×_comp [a b c d e f] (g: τ c → τ e) (g': τ d → τ f) (h: τ a → τ c) (h': τ b → τ d) (x: τ (a × b)) : π (map_× g g' (map_× h h' x) = map_× (λ u, g (h u)) (λ v, g' (h' v)) x) ≔ -begin assume a b c d e f g g' h h' x; reflexivity end; - -// symmetry +begin reflexivity end; symbol swap_× [a b] (x: τ (a × b)) : τ (b × a) ≔ (x ₂) ‚ (x ₁); -opaque symbol swap_×_invol [a b] (x: τ (a × b)) : π (swap_× (swap_× x) = x) ≔ -begin assume a b x; refine ×_η x end; - -// universal property: a map into a product is a pair of maps - -symbol pairing [a b c] (f: τ (c ⤳ a)) (g: τ (c ⤳ b)) : τ (c ⤳ (a × b)) ≔ +symbol pairing [a b c] (f: τ c → τ a) (g: τ c → τ b) : τ c → τ (a × b) ≔ λ z, f z ‚ g z; -opaque symbol ₁_pairing [a b c] (f: τ (c ⤳ a)) (g: τ (c ⤳ b)) (z: τ c) : +opaque symbol ₁_pairing [a b c] (f: τ c → τ a) (g: τ c → τ b) (z: τ c) : π ((pairing f g z ₁) = f z) ≔ -begin assume a b c f g z; reflexivity end; +begin reflexivity end; -opaque symbol ₂_pairing [a b c] (f: τ (c ⤳ a)) (g: τ (c ⤳ b)) (z: τ c) : +opaque symbol ₂_pairing [a b c] (f: τ c → τ a) (g: τ c → τ b) (z: τ c) : π ((pairing f g z ₂) = g z) ≔ -begin assume a b c f g z; reflexivity end; - -opaque symbol pairing_uniq [a b c] (h: τ (c ⤳ (a × b))) (z: τ c) : - π (pairing (λ u, h u ₁) (λ u, h u ₂) z = h z) ≔ -begin assume a b c h z; refine ×_η (h z) end; - - - -// Co-Cartesian product - -(a: Set) (b: Set) inductive Sum: TYPE ≔ -| inl: τ a → Sum a b -| inr: τ b → Sum a b -; - -constant symbol sum : Set → Set → Set; - -rule τ (sum $a $b) ↪ Sum $a $b; - -// Universal property: a map out of a sum is given by case analysis - -symbol sum_case [a b c] : τ (sum a b) → (τ a → τ c) → (τ b → τ c) → τ c; - -rule sum_case (inl $x) $f _ ↪ $f $x -with sum_case (inr $y) _ $g ↪ $g $y; - -opaque symbol sum_case_uniq [a b c] (h: τ (sum a b) → τ c) (s: τ (sum a b)) : - π (sum_case s (λ x, h (inl x)) (λ y, h (inr y)) = h s) ≔ -begin - assume a b c h; induction { assume x; reflexivity } { assume y; reflexivity } -end; - -opaque symbol sum_η [a b] (s: τ (sum a b)) : - π (sum_case s (λ x, inl x) (λ y, inr y) = s) ≔ -begin - assume a b; induction { assume x; reflexivity } { assume y; reflexivity } -end; - -// non confusion of constructors -symbol is_inl [a b] : τ (sum a b) → Prop; - -rule is_inl (inl _) ↪ ⊤ -with is_inl (inr _) ↪ ⊥; - -opaque symbol inr≠inl [a b] (x: τ a) (y: τ b) : π (@inr a b y ≠ inl x) ≔ -begin assume a b x y h; refine ind_eq h (λ s, is_inl s) ⊤ᵢ end; - -opaque symbol inl≠inr [a b] (x: τ a) (y: τ b) : π (@inl a b x ≠ inr y) ≔ -begin assume a b x y h; apply inr≠inl x y; symmetry; apply h end; - -symbol outl [a b] (s: τ (sum a b)) : τ a ≔ sum_case s (λ x, x) (λ _, el a); -symbol outr [a b] (s: τ (sum a b)) : τ b ≔ sum_case s (λ _, el b) (λ y, y); - -opaque symbol inl_inj [a b] (x x': τ a) : π (@inl a b x = inl x') → π (x = x') ≔ -begin assume a b x x' h; refine feq (λ s, @outl a b s) h end; - -opaque symbol inr_inj [a b] (y y': τ b) : π (@inr a b y = inr y') → π (y = y') ≔ -begin assume a b y y' h; refine feq (λ s, @outr a b s) h end; - -// induction principle with equalities - -opaque symbol case_Sum [a b] (s: τ (sum a b)) : - π ((`∃ x, s = inl x) ∨ (`∃ y, s = inr y)) ≔ -begin - assume a b; induction - { assume x; apply ∨ᵢ₁; apply ∃ᵢ x; reflexivity } - { assume y; apply ∨ᵢ₂; apply ∃ᵢ y; reflexivity } -end; - -opaque symbol ind_Sum_eq [a b] (p: τ (sum a b) → Prop) (s: τ (sum a b)) : - (Π x, π (s = inl x) → π (p s)) → (Π y, π (s = inr y) → π (p s)) → π (p s) ≔ -begin - assume a b p s hl hr; refine ∨ₑ (case_Sum s) (λ h, ∃ₑ h hl) (λ h, ∃ₑ h hr) -end; - -symbol map_sum [a b c d] (f: τ a → τ c) (g: τ b → τ d) (s: τ (sum a b)) - : τ (sum c d) ≔ sum_case s (λ x, inl (f x)) (λ y, inr (g y)); - -opaque symbol map_sum_id [a b] (s: τ (sum a b)) : - π (map_sum (λ u, u) (λ v, v) s = s) ≔ -begin assume a b s; refine sum_η s end; - -opaque symbol map_sum_comp [a b c d e f] - (g: τ c → τ e) (g': τ d → τ f) (h: τ a → τ c) (h': τ b → τ d) (s: τ (sum a b)) : - π (map_sum g g' (map_sum h h' s) = map_sum (λ u, g (h u)) (λ v, g' (h' v)) s) ≔ -begin - assume a b c d e f g g' h h'; - induction { assume x; reflexivity } { assume y; reflexivity } -end; - -symbol swap_sum [a b] (s: τ (sum a b)) : τ (sum b a) ≔ - sum_case s (λ x, inr x) (λ y, inl y); - -opaque symbol swap_sum_invol [a b] (s: τ (sum a b)) : - π (swap_sum (swap_sum s) = s) ≔ -begin - assume a b; induction { assume x; reflexivity } { assume y; reflexivity } -end; - -// Relation between the product and the coproduct -symbol dist_× [a b c] (x: τ (a × sum b c)) : τ (sum (a × b) (a × c)) ≔ - sum_case (x ₂) (λ y, inl ((x ₁) ‚ y)) (λ z, inr ((x ₁) ‚ z)); - -symbol undist_× [a b c] (s: τ (sum (a × b) (a × c))) : τ (a × sum b c) ≔ - sum_case s (λ u, (u ₁) ‚ inl (u ₂)) (λ v, (v ₁) ‚ inr (v ₂)); - -opaque symbol undist_dist_‚ [a b c] (u: τ a) (s: τ (sum b c)) : - π (undist_× (dist_× (u ‚ s)) = u ‚ s) ≔ -begin - assume a b c u; induction { assume y; reflexivity } { assume z; reflexivity } -end; - -opaque symbol undist_dist_× [a b c] (x: τ (a × sum b c)) : - π (undist_× (dist_× x) = x) ≔ -begin - assume a b c x; rewrite left (×_η x); refine undist_dist_‚ (x ₁) (x ₂) -end; - -opaque symbol dist_undist_× [a b c] (s: τ (sum (a × b) (a × c))) : - π (dist_× (undist_× s) = s) ≔ -begin - assume a b c; induction - { assume u; refine feq (λ w, @inl (a × b) (a × c) w) (×_η u) } - { assume v; refine feq (λ w, @inr (a × b) (a × c) w) (×_η v) } -end; - -symbol sum_curry [a b c] (h: τ (sum a b ⤳ c)) : τ ((a ⤳ c) × (b ⤳ c)) ≔ - (λ x, h (inl x)) ‚ (λ y, h (inr y)); - -symbol sum_uncurry [a b c] (fg: τ ((a ⤳ c) × (b ⤳ c))) : τ (sum a b ⤳ c) ≔ - λ s, sum_case s (fg ₁) (fg ₂); - -opaque symbol sum_uncurry_curry [a b c] (h: τ (sum a b ⤳ c)) (s: τ (sum a b)) : - π (sum_uncurry (sum_curry h) s = h s) ≔ -begin - assume a b c h; induction { assume x; reflexivity } { assume y; reflexivity } -end; - -opaque symbol sum_curry_uncurry₁ [a b c] (fg: τ ((a ⤳ c) × (b ⤳ c))) (x: τ a) : - π (((sum_curry (sum_uncurry fg)) ₁) x = (fg ₁) x) ≔ -begin assume a b c fg x; reflexivity end; - -opaque symbol sum_curry_uncurry₂ [a b c] (fg: τ ((a ⤳ c) × (b ⤳ c))) (y: τ b) : - π (((sum_curry (sum_uncurry fg)) ₂) y = (fg ₂) y) ≔ -begin assume a b c fg y; reflexivity end; - - - - - -// Dependent pair of an element and a proof - -[a: Set] (p: τ a → Prop) inductive Σ : TYPE ≔ - exist (x: τ a) : π (p x) → Σ p; - -symbol s₁ [a] [p] (e: @Σ a p) : τ a; -notation s₁ postfix 12; - -rule (exist $x _) s₁ ↪ $x; - -symbol s₂ [a] [p] (e: @Σ a p) : π (p (e s₁)); -notation s₂ postfix 12; - -rule (exist _ $h) s₂ ↪ $h; - -opaque symbol Σ_∃ [a] [p] (e: @Σ a p) : π (`∃ x, p x) ≔ -begin assume a p e; refine ∃ᵢ (e s₁) (e s₂) end; - -constant symbol Sigma [a] (p: τ a → Prop) : π (`∃ x, p x) → Set; - -rule τ (@Sigma $a $p _) ↪ @Σ $a $p; - -opaque symbol Σ_η [a] [p] [h] (e: τ (@Sigma a p h)) : π (exist (e s₁) (e s₂) = e) ≔ -begin assume a p h; induction; assume x hx; reflexivity end; - -opaque symbol eq_s₁ [a] [p] [h] (x y: τ (@Sigma a p h)) : π (x = y) → π (x s₁ = y s₁) ≔ -begin assume a p h x y e; refine feq (λ z, z s₁) e end; - -opaque symbol exist_inj [a] [p] [h] (x y: τ a) (hx: π (p x)) (hy: π (p y)) : - π (@= (@Sigma a p h) (exist x hx) (exist y hy)) → π (x = y) ≔ -begin assume a p h x y hx hy e; refine @eq_s₁ a p h (exist x hx) (exist y hy) e end; - - -// Dependent pair of an element and an element in Set - -[a: Set] (p: τ a → Set) inductive sigT : TYPE ≔ - exisT (x: τ a) : τ (p x) → sigT p; - -constant symbol SigmaT [a: Set] : (τ a → Set) → Set; - -rule τ (@SigmaT $a $p) ↪ @sigT $a $p; - - -symbol st₁ [a] [p] (e: @sigT a p) : τ a; -notation st₁ postfix 12; - -rule (exisT $x _) st₁ ↪ $x; - -symbol st₂ [a] [p] (e: @sigT a p) : τ (p (e st₁)); -notation st₂ postfix 12; - -rule (exisT _ $u) st₂ ↪ $u; - -opaque symbol sigT_η [a] [p] (e: @sigT a p) : π (exisT (e st₁) (e st₂) = e) ≔ -begin assume a p; induction; assume x u; reflexivity end; - -opaque symbol eq_st₁ [a] [p] (x y: @sigT a p) : π (x = y) → π (x st₁ = y st₁) ≔ -begin assume a p x y h; refine feq (λ e, e st₁) h end; - -symbol eq_exisT [a] [p] (x y: τ a) (u: τ (p x)) (v: τ (p y)) (h: π (x = y)) : - π (transport p h u = v) → π (@exisT a p x u = exisT y v); - -opaque symbol eq_exisT_refl [a] [p] (x: τ a) (u v: τ (p x)) : - π (u = v) → π (@exisT a p x u = exisT x v) ≔ -begin - assume a p x u v h; refine feq (λ w, @exisT a p x w) h -end; +begin reflexivity end; diff --git a/ProdExt.lp b/ProdExt.lp new file mode 100644 index 0000000..48b6474 --- /dev/null +++ b/ProdExt.lp @@ -0,0 +1,34 @@ +// Extensionality of the Cartesian product + +require open Stdlib.Prop Stdlib.Set Stdlib.HOL Stdlib.Eq Stdlib.FOL Stdlib.Prod; + +/* Surjective pairing. `×` has no interpretation rule for `τ`, so it is opaque + and η cannot be obtained by case analysis: we assume it. */ + +symbol prodExt [a b] (x: τ (a × b)) : π (x = (x ₁) ‚ (x ₂)); + +opaque symbol eq_pair [a b] (x y: τ (a × b)) : + π ((x ₁) = (y ₁)) → π ((x ₂) = (y ₂)) → π (x = y) ≔ +begin + assume a b x y h1 h2; + rewrite (prodExt x); rewrite (prodExt y); + refine feq2 (λ u v, u ‚ v) h1 h2 +end; + +opaque symbol eq_×_iff [a b] (x y: τ (a × b)) : + π (x = y ⇔ (x ₁) = (y ₁) ∧ (x ₂) = (y ₂)) ≔ +begin + assume a b x y; apply ∧ᵢ + { assume h; apply ∧ᵢ { refine eq_₁ x y h } { refine eq_₂ x y h } } + { assume h; refine eq_pair x y (∧ₑ₁ h) (∧ₑ₂ h) } +end; + +opaque symbol map_×_id [a b] (x: τ (a × b)) : π (map_× (λ u, u) (λ v, v) x = x) ≔ +begin assume a b x; symmetry; refine prodExt x end; + +opaque symbol swap_×_invol [a b] (x: τ (a × b)) : π (swap_× (swap_× x) = x) ≔ +begin assume a b x; symmetry; refine prodExt x end; + +opaque symbol pairing_uniq [a b c] (h: τ (c ⤳ (a × b))) (z: τ c) : + π (pairing (λ u, h u ₁) (λ u, h u ₂) z = h z) ≔ +begin assume a b c h z; symmetry; refine prodExt (h z) end; diff --git a/Subset.lp b/Subset.lp new file mode 100644 index 0000000..9ae5d3c --- /dev/null +++ b/Subset.lp @@ -0,0 +1,37 @@ +// Subset types: a dependent pair of an element and a proof + +require open Stdlib.Prop Stdlib.Set Stdlib.Eq Stdlib.FOL; + +[a: Set] (p: τ a → Prop) inductive Subset : TYPE ≔ + mk (x: τ a) : π (p x) → Subset p; + +symbol elt [a] [p] (e: @Subset a p) : τ a; + +rule elt (mk $x _) ↪ $x; + +symbol prf [a] [p] (e: @Subset a p) : π (p (elt e)); + +rule prf (mk _ $h) ↪ $h; + +opaque symbol Subset_∃ [a] [p] (e: @Subset a p) : π (`∃ x, p x) ≔ +begin assume a p e; refine ∃ᵢ (elt e) (prf e) end; + +/* The `subset` Set-constructor requires an existential proof: this is needed + to be consistent with the axiom `el` of Set.lp stating that every set is + non-empty. */ + +constant symbol subset [a] (p: τ a → Prop) : π (`∃ x, p x) → Set; + +rule τ (@subset $a $p _) ↪ @Subset $a $p; + +opaque symbol Subset_η [a] [p] [h] (e: τ (@subset a p h)) : + π (mk (elt e) (prf e) = e) ≔ +begin assume a p h; induction; assume x hx; reflexivity end; + +opaque symbol eq_elt [a] [p] [h] (x y: τ (@subset a p h)) : + π (x = y) → π (elt x = elt y) ≔ +begin assume a p h x y e; refine feq (λ z, elt z) e end; + +opaque symbol mk_inj [a] [p] [h] (x y: τ a) (hx: π (p x)) (hy: π (p y)) : + π (@= (@subset a p h) (mk x hx) (mk y hy)) → π (x = y) ≔ +begin assume a p h x y hx hy e; refine @eq_elt a p h (mk x hx) (mk y hy) e end; diff --git a/Z.lp b/Z.lp index 9929066..e9350ca 100644 --- a/Z.lp +++ b/Z.lp @@ -34,20 +34,6 @@ builtin "int_zero" ≔ Z0; builtin "int_positive" ≔ Zpos; builtin "int_negative" ≔ Zneg; -// enable parsing of integers in decimal notation - -builtin "0" ≔ Z0; -builtin "1" ≔ _1; -builtin "2" ≔ _2; -builtin "3" ≔ _3; -builtin "4" ≔ _4; -builtin "5" ≔ _5; -builtin "6" ≔ _6; -builtin "7" ≔ _7; -builtin "8" ≔ _8; -builtin "9" ≔ _9; -builtin "10" ≔ _10; - // boolean functions for testing head constructor symbol isZ0 : ℤ → 𝔹; @@ -424,6 +410,20 @@ notation * infix right 22; builtin "*" ≔ *; +// enable parsing of integers in decimal notation + +builtin "0" ≔ Z0; +builtin "1" ≔ _1; +builtin "2" ≔ _2; +builtin "3" ≔ _3; +builtin "4" ≔ _4; +builtin "5" ≔ _5; +builtin "6" ≔ _6; +builtin "7" ≔ _7; +builtin "8" ≔ _8; +builtin "9" ≔ _9; +builtin "10" ≔ _10; + rule Z0 * _ ↪ Z0 with _ * Z0 ↪ Z0 with Zpos $x * Zpos $y ↪ Zpos (mul $x $y) @@ -488,7 +488,10 @@ end; opaque symbol *_neutral x : π (x * Zpos H = x) ≔ begin - induction { reflexivity } { reflexivity } { reflexivity } + induction + { reflexivity } + { assume p; simplify; rewrite mul_H_right; reflexivity } + { assume p; simplify; rewrite mul_H_right; reflexivity } end; opaque symbol *Z0 x : π (x * Z0 = Z0) ≔ @@ -797,6 +800,27 @@ begin { assume a r; reflexivity } end; +// ℤ has no zero divisor + +opaque symbol *=Z0 x y : π (x * y = Z0) → π (x = Z0 ∨ y = Z0) ≔ +begin + induction + // case Z0 + { assume y h; apply ∨ᵢ₁; reflexivity } + // case Zpos + { assume a; + induction + { assume h; apply ∨ᵢ₂; reflexivity } + { assume b h; apply ⊥ₑ (Zpos≠Z0 (mul a b) h) } + { assume b h; apply ⊥ₑ (Zneg≠Z0 (mul a b) h) } } + // case Zneg + { assume a; + induction + { assume h; apply ∨ᵢ₂; reflexivity } + { assume b h; apply ⊥ₑ (Zneg≠Z0 (mul a b) h) } + { assume b h; apply ⊥ₑ (Zpos≠Z0 (mul a b) h) } } +end; + opaque symbol ≐_refl x : π (x ≐ x = Eq) ≔ begin induction From 360919a7c31da97751170e190b87bfb96b1aa969 Mon Sep 17 00:00:00 2001 From: NotBad4U Date: Tue, 29 Sep 2026 16:10:55 +0200 Subject: [PATCH 03/13] Update mergesort and fix coprod deps --- Coprod.lp | 22 +++++++++++----------- List.lp | 4 ++-- 2 files changed, 13 insertions(+), 13 deletions(-) diff --git a/Coprod.lp b/Coprod.lp index 4139dd6..a57c178 100644 --- a/Coprod.lp +++ b/Coprod.lp @@ -1,6 +1,6 @@ // Co-Cartesian product (disjoint sum) -require open Stdlib.Prod; +require open Stdlib.Prod Stdlib.FOL; (a: Set) (b: Set) inductive Sum: TYPE ≔ | inl: τ a → Sum a b @@ -107,22 +107,22 @@ end; // currying -symbol sum_curry [a b c] (h: τ (sum a b ⤳ c)) : τ ((a ⤳ c) × (b ⤳ c)) ≔ - (λ x, h (inl x)) ‚ (λ y, h (inr y)); +symbol sum_curry₁ [a b c] (h: τ (sum a b) → τ c) (x: τ a) : τ c ≔ h (inl x); +symbol sum_curry₂ [a b c] (h: τ (sum a b) → τ c) (y: τ b) : τ c ≔ h (inr y); -symbol sum_uncurry [a b c] (fg: τ ((a ⤳ c) × (b ⤳ c))) : τ (sum a b ⤳ c) ≔ - λ s, sum_case s (fg ₁) (fg ₂); +symbol sum_uncurry [a b c] (f: τ a → τ c) (g: τ b → τ c) (s: τ (sum a b)) : τ c ≔ + sum_case s f g; -opaque symbol sum_uncurry_curry [a b c] (h: τ (sum a b ⤳ c)) (s: τ (sum a b)) : - π (sum_uncurry (sum_curry h) s = h s) ≔ +opaque symbol sum_uncurry_curry [a b c] (h: τ (sum a b) → τ c) (s: τ (sum a b)) : + π (sum_uncurry (sum_curry₁ h) (sum_curry₂ h) s = h s) ≔ begin assume a b c h; induction { reflexivity } { reflexivity } end; -opaque symbol sum_curry_uncurry₁ [a b c] (fg: τ ((a ⤳ c) × (b ⤳ c))) (x: τ a) : - π (((sum_curry (sum_uncurry fg)) ₁) x = (fg ₁) x) ≔ +opaque symbol sum_curry_uncurry₁ [a b c] (f: τ a → τ c) (g: τ b → τ c) (x: τ a) : + π (sum_curry₁ (sum_uncurry f g) x = f x) ≔ begin reflexivity end; -opaque symbol sum_curry_uncurry₂ [a b c] (fg: τ ((a ⤳ c) × (b ⤳ c))) (y: τ b) : - π (((sum_curry (sum_uncurry fg)) ₂) y = (fg ₂) y) ≔ +opaque symbol sum_curry_uncurry₂ [a b c] (f: τ a → τ c) (g: τ b → τ c) (y: τ b) : + π (sum_curry₂ (sum_uncurry f g) y = g y) ≔ begin reflexivity end; diff --git a/List.lp b/List.lp index ed69395..8396b8d 100644 --- a/List.lp +++ b/List.lp @@ -1956,8 +1956,8 @@ symbol mergesort [a] : (τ a → τ a → 𝔹) → 𝕃 a → 𝕃 a; rule mergesort _ □ ↪ □ with mergesort _ ($x ⸬ □) ↪ $x ⸬ □ with mergesort $≤ ($x ⸬ $y ⸬ $l) ↪ - merge $≤ (mergesort $≤ ($x ⸬ ((split $l)₁))) - (mergesort $≤ ($y ⸬ ((split $l)₂))); + let s ≔ split ($x ⸬ $y ⸬ $l) in + merge $≤ (mergesort $≤ (s ₁)) (mergesort $≤ (s ₂)); assert ⊢ mergesort (≤) (3 ⸬ 1 ⸬ 4 ⸬ 1 ⸬ 5 ⸬ □) ≡ 1 ⸬ 1 ⸬ 3 ⸬ 4 ⸬ 5 ⸬ □; From 16d8eb7235bb6b88340fa1854c6c667a4465267b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Thu, 1 Oct 2026 14:10:51 +0200 Subject: [PATCH 04/13] remove useless require --- HOL.lp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/HOL.lp b/HOL.lp index 156135b..08dd3bf 100644 --- a/HOL.lp +++ b/HOL.lp @@ -1,4 +1,4 @@ -require open Stdlib.Set Stdlib.Eq; +require open Stdlib.Set; constant symbol ⤳ : Set → Set → Set; // \leadsto From c35c9508ff82ae0d65d57043fa8356cc8a35bcd0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Thu, 1 Oct 2026 14:11:31 +0200 Subject: [PATCH 05/13] CHANGES: record only changes wrt previous release --- CHANGES.md | 8 -------- 1 file changed, 8 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index a20c716..63488e8 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -27,14 +27,6 @@ and this project adheres to [Semantic Versioning](https://semver.org/). - Changed rewrite rules to be in line with the Rocq standard library. - Moved rules not in line with Rocq to the module ExtraRules. -- Bool: imp is now defined from not and or, and xorb uses more general rules, - to be in line with Rocq. -- Nat and Z: the builtins for parsing decimal numbers are now declared - together with those for + and *. -- Pos: moved the rule `mul x H ↪ x` to ExtraRules. -- Prod: the co-Cartesian product, subset types and dependent products have - been moved to the new modules Coprod, Subset and DepProd, and the - properties requiring surjective pairing to the new module ProdExt. ## 1.4.0 (2026-07-07) From 02cef9a50ec3a050eac22851793d02b41c4b9922 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Thu, 1 Oct 2026 14:29:22 +0200 Subject: [PATCH 06/13] remove useless requires --- ProdExt.lp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/ProdExt.lp b/ProdExt.lp index 48b6474..99c7dec 100644 --- a/ProdExt.lp +++ b/ProdExt.lp @@ -1,6 +1,6 @@ // Extensionality of the Cartesian product -require open Stdlib.Prop Stdlib.Set Stdlib.HOL Stdlib.Eq Stdlib.FOL Stdlib.Prod; +require open Stdlib.FOL Stdlib.Eq Stdlib.Prod; /* Surjective pairing. `×` has no interpretation rule for `τ`, so it is opaque and η cannot be obtained by case analysis: we assume it. */ @@ -29,6 +29,6 @@ begin assume a b x; symmetry; refine prodExt x end; opaque symbol swap_×_invol [a b] (x: τ (a × b)) : π (swap_× (swap_× x) = x) ≔ begin assume a b x; symmetry; refine prodExt x end; -opaque symbol pairing_uniq [a b c] (h: τ (c ⤳ (a × b))) (z: τ c) : +opaque symbol pairing_uniq [a b c] (h: τ c → τ (a × b)) (z: τ c) : π (pairing (λ u, h u ₁) (λ u, h u ₂) z = h z) ≔ begin assume a b c h z; symmetry; refine prodExt (h z) end; From 32041cce2dbda65d5208e59add1638d53e6ec4ba Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Thu, 1 Oct 2026 14:30:27 +0200 Subject: [PATCH 07/13] remove useless explicit arguments --- CoprodExt.lp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/CoprodExt.lp b/CoprodExt.lp index 209e98f..540bc9c 100644 --- a/CoprodExt.lp +++ b/CoprodExt.lp @@ -5,13 +5,13 @@ require open Stdlib.ProdExt Stdlib.Coprod; opaque symbol undist_dist_× [a b c] (x: τ (a × sum b c)) : π (undist_× (dist_× x) = x) ≔ begin - assume a b c x; rewrite (prodExt x); refine undist_dist_‚ (x ₁) (x ₂) + assume a b c x; rewrite prodExt x; refine undist_dist_‚ (x ₁) (x ₂) end; opaque symbol dist_undist_× [a b c] (s: τ (sum (a × b) (a × c))) : π (dist_× (undist_× s) = s) ≔ begin assume a b c; induction - { assume u; symmetry; refine feq (λ w, @inl (a × b) (a × c) w) (prodExt u) } - { assume v; symmetry; refine feq (λ w, @inr (a × b) (a × c) w) (prodExt v) } + { assume u; symmetry; refine feq inl (prodExt u) } + { assume v; symmetry; refine feq inr (prodExt v) } end; From 7afda8c3e3b1fe716a4c4105f273cbebd362b828 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Thu, 1 Oct 2026 14:31:07 +0200 Subject: [PATCH 08/13] moved relation between sum and prod at the end --- Coprod.lp | 36 +++++++++++++++++++----------------- 1 file changed, 19 insertions(+), 17 deletions(-) diff --git a/Coprod.lp b/Coprod.lp index a57c178..d6138de 100644 --- a/Coprod.lp +++ b/Coprod.lp @@ -1,11 +1,10 @@ // Co-Cartesian product (disjoint sum) -require open Stdlib.Prod Stdlib.FOL; +require open Stdlib.FOL Stdlib.Eq; (a: Set) (b: Set) inductive Sum: TYPE ≔ | inl: τ a → Sum a b -| inr: τ b → Sum a b -; +| inr: τ b → Sum a b; constant symbol sum : Set → Set → Set; @@ -31,6 +30,7 @@ begin end; // non confusion of constructors + symbol is_inl [a b] : τ (sum a b) → Prop; rule is_inl (inl _) ↪ ⊤ @@ -91,20 +91,6 @@ begin assume a b; induction { reflexivity } { reflexivity } end; -// Relation between the product and the coproduct - -symbol dist_× [a b c] (x: τ (a × sum b c)) : τ (sum (a × b) (a × c)) ≔ - sum_case (x ₂) (λ y, inl ((x ₁) ‚ y)) (λ z, inr ((x ₁) ‚ z)); - -symbol undist_× [a b c] (s: τ (sum (a × b) (a × c))) : τ (a × sum b c) ≔ - sum_case s (λ u, (u ₁) ‚ inl (u ₂)) (λ v, (v ₁) ‚ inr (v ₂)); - -opaque symbol undist_dist_‚ [a b c] (u: τ a) (s: τ (sum b c)) : - π (undist_× (dist_× (u ‚ s)) = u ‚ s) ≔ -begin - assume a b c u; induction { reflexivity } { reflexivity } -end; - // currying symbol sum_curry₁ [a b c] (h: τ (sum a b) → τ c) (x: τ a) : τ c ≔ h (inl x); @@ -126,3 +112,19 @@ begin reflexivity end; opaque symbol sum_curry_uncurry₂ [a b c] (f: τ a → τ c) (g: τ b → τ c) (y: τ b) : π (sum_curry₂ (sum_uncurry f g) y = g y) ≔ begin reflexivity end; + +// Relation between the product and the coproduct + +require open Stdlib.Prod; + +symbol dist_× [a b c] (x: τ (a × sum b c)) : τ (sum (a × b) (a × c)) ≔ + sum_case (x ₂) (λ y, inl ((x ₁) ‚ y)) (λ z, inr ((x ₁) ‚ z)); + +symbol undist_× [a b c] (s: τ (sum (a × b) (a × c))) : τ (a × sum b c) ≔ + sum_case s (λ u, (u ₁) ‚ inl (u ₂)) (λ v, (v ₁) ‚ inr (v ₂)); + +opaque symbol undist_dist_‚ [a b c] (u: τ a) (s: τ (sum b c)) : + π (undist_× (dist_× (u ‚ s)) = u ‚ s) ≔ +begin + assume a b c u; induction { reflexivity } { reflexivity } +end; From 42735f14eb2003546ff9c62dedea2e2bdf9db045 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Thu, 1 Oct 2026 14:51:47 +0200 Subject: [PATCH 09/13] derive ProdExt by defining Prod inductively --- Coprod.lp | 14 ++++++++++++++ CoprodExt.lp | 17 ----------------- Prod.lp | 41 +++++++++++++++++++++++++++++++++++++---- ProdExt.lp | 34 ---------------------------------- 4 files changed, 51 insertions(+), 55 deletions(-) delete mode 100644 CoprodExt.lp delete mode 100644 ProdExt.lp diff --git a/Coprod.lp b/Coprod.lp index d6138de..d12645b 100644 --- a/Coprod.lp +++ b/Coprod.lp @@ -128,3 +128,17 @@ opaque symbol undist_dist_‚ [a b c] (u: τ a) (s: τ (sum b c)) : begin assume a b c u; induction { reflexivity } { reflexivity } end; + +opaque symbol undist_dist_× [a b c] (x: τ (a × sum b c)) : + π (undist_× (dist_× x) = x) ≔ +begin + assume a b c x; rewrite prodExt x; refine undist_dist_‚ (x ₁) (x ₂) +end; + +opaque symbol dist_undist_× [a b c] (s: τ (sum (a × b) (a × c))) : + π (dist_× (undist_× s) = s) ≔ +begin + assume a b c; induction + { assume u; symmetry; refine feq inl (prodExt u) } + { assume v; symmetry; refine feq inr (prodExt v) } +end; diff --git a/CoprodExt.lp b/CoprodExt.lp deleted file mode 100644 index 540bc9c..0000000 --- a/CoprodExt.lp +++ /dev/null @@ -1,17 +0,0 @@ -/* Properties of the co-Cartesian product that require the extensionality of the Cartesian product. */ - -require open Stdlib.ProdExt Stdlib.Coprod; - -opaque symbol undist_dist_× [a b c] (x: τ (a × sum b c)) : - π (undist_× (dist_× x) = x) ≔ -begin - assume a b c x; rewrite prodExt x; refine undist_dist_‚ (x ₁) (x ₂) -end; - -opaque symbol dist_undist_× [a b c] (s: τ (sum (a × b) (a × c))) : - π (dist_× (undist_× s) = s) ≔ -begin - assume a b c; induction - { assume u; symmetry; refine feq inl (prodExt u) } - { assume v; symmetry; refine feq inr (prodExt v) } -end; diff --git a/Prod.lp b/Prod.lp index 94592f4..af2a3c3 100644 --- a/Prod.lp +++ b/Prod.lp @@ -1,12 +1,14 @@ // Cartesian product -require open Stdlib.Prop Stdlib.Set Stdlib.Eq; +require open Stdlib.Eq; -constant symbol × : Set → Set → Set; notation × infix right 10; // \times +(a b:Set) inductive Prod:TYPE ≔ ‚ : τ a → τ b → Prod a b; + +notation ‚ infix right 30; -assert a b c ⊢ a × b × c ≡ a × (b × c); +constant symbol × : Set → Set → Set; notation × infix right 10; // \times -symbol ‚ [a b] : τ a → τ b → τ (a × b); notation ‚ infix right 30; +rule τ ($a × $b) ↪ Prod $a $b; assert a (x:τ a) b (y:τ b) c (z:τ c) ⊢ x ‚ y ‚ z : τ(a × b × c); assert x y z ⊢ x ‚ y ‚ z ≡ x ‚ (y ‚ z); @@ -53,3 +55,34 @@ begin reflexivity end; opaque symbol ₂_pairing [a b c] (f: τ c → τ a) (g: τ c → τ b) (z: τ c) : π ((pairing f g z ₂) = g z) ≔ begin reflexivity end; + +symbol prodExt [a b] (x: τ (a × b)) : π (x = (x ₁) ‚ (x ₂)) ≔ +begin + assume a; refine ind_Prod a (λ b x, x = (x ₁) ‚ (x ₂)) _; reflexivity +end; + +opaque symbol eq_pair [a b] (x y: τ (a × b)) : + π ((x ₁) = (y ₁)) → π ((x ₂) = (y ₂)) → π (x = y) ≔ +begin + assume a b x y h1 h2; + rewrite (prodExt x); rewrite (prodExt y); + refine feq2 (λ u v, u ‚ v) h1 h2 +end; + +opaque symbol eq_×_iff [a b] (x y: τ (a × b)) : + π (x = y ⇔ (x ₁) = (y ₁) ∧ (x ₂) = (y ₂)) ≔ +begin + assume a b x y; apply ∧ᵢ + { assume h; apply ∧ᵢ { refine eq_₁ x y h } { refine eq_₂ x y h } } + { assume h; refine eq_pair x y (∧ₑ₁ h) (∧ₑ₂ h) } +end; + +opaque symbol map_×_id [a b] (x: τ (a × b)) : π (map_× (λ u, u) (λ v, v) x = x) ≔ +begin assume a b x; symmetry; refine prodExt x end; + +opaque symbol swap_×_invol [a b] (x: τ (a × b)) : π (swap_× (swap_× x) = x) ≔ +begin assume a b x; symmetry; refine prodExt x end; + +opaque symbol pairing_uniq [a b c] (h: τ c → τ (a × b)) (z: τ c) : + π (pairing (λ u, h u ₁) (λ u, h u ₂) z = h z) ≔ +begin assume a b c h z; symmetry; refine prodExt (h z) end; diff --git a/ProdExt.lp b/ProdExt.lp deleted file mode 100644 index 99c7dec..0000000 --- a/ProdExt.lp +++ /dev/null @@ -1,34 +0,0 @@ -// Extensionality of the Cartesian product - -require open Stdlib.FOL Stdlib.Eq Stdlib.Prod; - -/* Surjective pairing. `×` has no interpretation rule for `τ`, so it is opaque - and η cannot be obtained by case analysis: we assume it. */ - -symbol prodExt [a b] (x: τ (a × b)) : π (x = (x ₁) ‚ (x ₂)); - -opaque symbol eq_pair [a b] (x y: τ (a × b)) : - π ((x ₁) = (y ₁)) → π ((x ₂) = (y ₂)) → π (x = y) ≔ -begin - assume a b x y h1 h2; - rewrite (prodExt x); rewrite (prodExt y); - refine feq2 (λ u v, u ‚ v) h1 h2 -end; - -opaque symbol eq_×_iff [a b] (x y: τ (a × b)) : - π (x = y ⇔ (x ₁) = (y ₁) ∧ (x ₂) = (y ₂)) ≔ -begin - assume a b x y; apply ∧ᵢ - { assume h; apply ∧ᵢ { refine eq_₁ x y h } { refine eq_₂ x y h } } - { assume h; refine eq_pair x y (∧ₑ₁ h) (∧ₑ₂ h) } -end; - -opaque symbol map_×_id [a b] (x: τ (a × b)) : π (map_× (λ u, u) (λ v, v) x = x) ≔ -begin assume a b x; symmetry; refine prodExt x end; - -opaque symbol swap_×_invol [a b] (x: τ (a × b)) : π (swap_× (swap_× x) = x) ≔ -begin assume a b x; symmetry; refine prodExt x end; - -opaque symbol pairing_uniq [a b c] (h: τ c → τ (a × b)) (z: τ c) : - π (pairing (λ u, h u ₁) (λ u, h u ₂) z = h z) ≔ -begin assume a b c h z; symmetry; refine prodExt (h z) end; From 2b684cb710e05330a8702cc71609fba47074f515 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Thu, 1 Oct 2026 14:52:21 +0200 Subject: [PATCH 10/13] update CHANGES --- CHANGES.md | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index 63488e8..a090b18 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -17,8 +17,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/). - Nat: parity, div2, shifts, bitwise operations and strong induction - Pos: theorems on multiplication - Prod: theorems on the Cartesian product -- ProdExt: extensionality of the Cartesian product -- Coprod and CoprodExt: the co-Cartesian product (disjoint sum) +- Coprod: the co-Cartesian product (disjoint sum) - Subset: subset types - DepProd: dependent products and transport - Z: theorems on multiplication, power and comparison From 8f293f1ecc78fc46318d662c9750bf6a0af05560 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Fri, 2 Oct 2026 09:55:21 +0200 Subject: [PATCH 11/13] details --- DepProd.lp | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) diff --git a/DepProd.lp b/DepProd.lp index 5dc7591..4281615 100644 --- a/DepProd.lp +++ b/DepProd.lp @@ -1,10 +1,6 @@ // Dependent product: a dependent pair of an element and an element in Set -require open Stdlib.Prop Stdlib.Set Stdlib.Eq; - - -symbol transport [a] (p: τ a → Set) [x y: τ a] : π (x = y) → τ (p x) → τ (p y); -rule transport _ (eq_refl _) $u ↪ $u; +require open Stdlib.Eq; [a: Set] (p: τ a → Set) inductive DProd : TYPE ≔ dpair (x: τ a) : τ (p x) → DProd p; @@ -29,11 +25,14 @@ opaque symbol eq_proj₁ [a] [p] (x y: @DProd a p) : π (x = y) → π (proj₁ x = proj₁ y) ≔ begin assume a p x y h; refine feq (λ e, proj₁ e) h end; -symbol eq_dpair [a] [p] (x y: τ a) (u: τ (p x)) (v: τ (p y)) (h: π (x = y)) : - π (transport p h u = v) → π (@dpair a p x u = dpair y v); - opaque symbol eq_dpair_refl [a] [p] (x: τ a) (u v: τ (p x)) : π (u = v) → π (@dpair a p x u = dpair x v) ≔ begin assume a p x u v h; refine feq (λ w, @dpair a p x w) h end; + +symbol transport [a] (p: τ a → Set) [x y: τ a] : π (x = y) → τ (p x) → τ (p y); +rule transport _ (eq_refl _) $u ↪ $u; + +symbol eq_dpair [a] [p] (x y: τ a) (u: τ (p x)) (v: τ (p y)) (h: π (x = y)) : + π (transport p h u = v) → π (@dpair a p x u = dpair y v); From c8a10c591d15379c1bdfba528391aaf5a09de1ca Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Fri, 2 Oct 2026 10:15:05 +0200 Subject: [PATCH 12/13] details --- Coprod.lp | 4 ++-- DepProd.lp | 2 +- Subset.lp | 22 +++++++++++----------- 3 files changed, 14 insertions(+), 14 deletions(-) diff --git a/Coprod.lp b/Coprod.lp index d12645b..a2ad23f 100644 --- a/Coprod.lp +++ b/Coprod.lp @@ -23,7 +23,7 @@ begin assume a b c h; induction { reflexivity } { reflexivity } end; -opaque symbol sum_η [a b] (s: τ (sum a b)) : +opaque symbol η_sum [a b] (s: τ (sum a b)) : π (sum_case s (λ x, inl x) (λ y, inr y) = s) ≔ begin assume a b; induction { reflexivity } { reflexivity } @@ -72,7 +72,7 @@ symbol map_sum [a b c d] (f: τ a → τ c) (g: τ b → τ d) (s: τ (sum a b)) opaque symbol map_sum_id [a b] (s: τ (sum a b)) : π (map_sum (λ u, u) (λ v, v) s = s) ≔ -begin assume a b s; refine sum_η s end; +begin assume a b s; refine η_sum s end; opaque symbol map_sum_comp [a b c d e f] (g: τ c → τ e) (g': τ d → τ f) (h: τ a → τ c) (h': τ b → τ d) (s: τ (sum a b)) : diff --git a/DepProd.lp b/DepProd.lp index 4281615..b32b265 100644 --- a/DepProd.lp +++ b/DepProd.lp @@ -17,7 +17,7 @@ symbol proj₂ [a] [p] (e: @DProd a p) : τ (p (proj₁ e)); rule proj₂ (dpair _ $u) ↪ $u; -opaque symbol DProd_η [a] [p] (e: @DProd a p) : +opaque symbol η_dprod [a] [p] (e: @DProd a p) : π (dpair (proj₁ e) (proj₂ e) = e) ≔ begin assume a p; induction; assume x u; reflexivity end; diff --git a/Subset.lp b/Subset.lp index 9ae5d3c..300fab9 100644 --- a/Subset.lp +++ b/Subset.lp @@ -1,19 +1,19 @@ // Subset types: a dependent pair of an element and a proof -require open Stdlib.Prop Stdlib.Set Stdlib.Eq Stdlib.FOL; +require open Stdlib.FOL Stdlib.Eq; [a: Set] (p: τ a → Prop) inductive Subset : TYPE ≔ mk (x: τ a) : π (p x) → Subset p; -symbol elt [a] [p] (e: @Subset a p) : τ a; +symbol elt [a] [p:τ a → Prop] (e: Subset p) : τ a; rule elt (mk $x _) ↪ $x; -symbol prf [a] [p] (e: @Subset a p) : π (p (elt e)); +symbol prf [a] [p:τ a → Prop] (e: Subset p) : π (p (elt e)); rule prf (mk _ $h) ↪ $h; -opaque symbol Subset_∃ [a] [p] (e: @Subset a p) : π (`∃ x, p x) ≔ +opaque symbol Subset_∃ [a] [p:τ a → Prop] (e: Subset p) : π (`∃ x, p x) ≔ begin assume a p e; refine ∃ᵢ (elt e) (prf e) end; /* The `subset` Set-constructor requires an existential proof: this is needed @@ -22,16 +22,16 @@ begin assume a p e; refine ∃ᵢ (elt e) (prf e) end; constant symbol subset [a] (p: τ a → Prop) : π (`∃ x, p x) → Set; -rule τ (@subset $a $p _) ↪ @Subset $a $p; +rule τ (subset $p _) ↪ Subset $p; -opaque symbol Subset_η [a] [p] [h] (e: τ (@subset a p h)) : +opaque symbol η_subset [a] [p:τ a → Prop] [h] (e: τ (subset p h)) : π (mk (elt e) (prf e) = e) ≔ -begin assume a p h; induction; assume x hx; reflexivity end; +begin assume a p h; induction; reflexivity end; -opaque symbol eq_elt [a] [p] [h] (x y: τ (@subset a p h)) : +opaque symbol eq_elt [a] [p:τ a → Prop] [h] (x y: τ (subset p h)) : π (x = y) → π (elt x = elt y) ≔ -begin assume a p h x y e; refine feq (λ z, elt z) e end; +begin assume a p h x y e; refine feq elt e end; -opaque symbol mk_inj [a] [p] [h] (x y: τ a) (hx: π (p x)) (hy: π (p y)) : - π (@= (@subset a p h) (mk x hx) (mk y hy)) → π (x = y) ≔ +opaque symbol mk_inj [a] [p:τ a → Prop] [h] x y (hx: π (p x)) (hy: π (p y)) : + π (= [subset p h] (mk x hx) (mk y hy)) → π (x = y) ≔ begin assume a p h x y hx hy e; refine @eq_elt a p h (mk x hx) (mk y hy) e end; From 496c0faad9dfc8c285e0aa1e8893759cf3c60c89 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Fri, 2 Oct 2026 10:32:12 +0200 Subject: [PATCH 13/13] details --- Nat.lp | 50 +++++++++++++++++++++----------------------------- Z.lp | 44 ++++++++++++++++---------------------------- 2 files changed, 37 insertions(+), 57 deletions(-) diff --git a/Nat.lp b/Nat.lp index 59a160c..d41423b 100644 --- a/Nat.lp +++ b/Nat.lp @@ -95,12 +95,10 @@ inductive ℕ : TYPE ≔ | +1 : ℕ → ℕ; notation +1 postfix 100; // enable printing of natural numbers in decimal notation - builtin "nat_zero" ≔ _0; builtin "nat_succ" ≔ +1; // shortcuts - symbol _1 ≔ _0 +1; symbol _2 ≔ _1 +1; symbol _3 ≔ _2 +1; @@ -229,8 +227,6 @@ symbol + : ℕ → ℕ → ℕ; notation + infix left 20; rule _0 + $y ↪ $y with $x +1 + $y ↪ ($x + $y) +1; -builtin "+" ≔ +; - opaque symbol add0n x : π (_0 + x = x) ≔ begin assume x; reflexivity; @@ -571,22 +567,6 @@ assert x y z ⊢ x + y * z ≡ x + (y * z); rule _0 * _ ↪ _0 with ($x +1) * $y ↪ $y + $x * $y; -builtin "*" ≔ *; - -// enable parsing of natural numbers in decimal notation - -builtin "0" ≔ _0; -builtin "1" ≔ _1; -builtin "2" ≔ _2; -builtin "3" ≔ _3; -builtin "4" ≔ _4; -builtin "5" ≔ _5; -builtin "6" ≔ _6; -builtin "7" ≔ _7; -builtin "8" ≔ _8; -builtin "9" ≔ _9; -builtin "10" ≔ _10; - opaque symbol mul0n x : π (x * _0 = _0) ≔ begin induction { reflexivity } { assume x' h; apply h } @@ -626,7 +606,7 @@ begin { assume x' h y; simplify; rewrite h; rewrite addnAC; reflexivity } end; -opaque symbol muln2 n: π (n * 2 = n + n) ≔ +opaque symbol muln2 n: π (n * _2 = n + n) ≔ begin assume n; simplify; rewrite mulnS; rewrite muln1; reflexivity end; @@ -726,6 +706,22 @@ begin }; end; +// enable parsing of decimal notation + +builtin "0" ≔ _0; +builtin "1" ≔ _1; +builtin "2" ≔ _2; +builtin "3" ≔ _3; +builtin "4" ≔ _4; +builtin "5" ≔ _5; +builtin "6" ≔ _6; +builtin "7" ≔ _7; +builtin "8" ≔ _8; +builtin "9" ≔ _9; +builtin "10" ≔ _10; +builtin "+" ≔ +; +builtin "*" ≔ *; + // Boolean ordering functions symbol ≤ : ℕ → ℕ → 𝔹; notation ≤ infix left 10; @@ -1199,12 +1195,8 @@ end; opaque symbol exD_leq n m : π (`∃ p, n + p = m) → π (n ≤ m) ≔ begin - assume n m h; - refine ∃ₑ h _; - assume p h2; - remove h; - rewrite left h2; - refine leq_addr p n; + assume n m h; refine ∃ₑ h _; assume p h2; remove h; + rewrite left h2; refine leq_addr p n; end; // max @@ -1999,7 +1991,7 @@ end; symbol double x ≔ x + x; // shift left -// left-shifting an natural `x` with an natural `y` is equivalent to multiplying `x` with 2 raised to power `y`. +// left-shifting a natural `x` with a natural `y` is equivalent to multiplying `x` by 2 raised to power `y`. symbol <<<: ℕ → ℕ → ℕ; notation <<< infix 30; rule $x <<< 0 ↪ $x with $x <<< ($n +1) ↪ double ($x <<< $n); @@ -2032,7 +2024,6 @@ assert ⊢ 2 ⎪⎪ 8 ≡ 10; symbol diff (a b: ℕ): ℕ ≔ bitwise (λ b1, λ b2, b1 and (not b2)) a a b; -// Definition lxor a b := bitwise xorb (max a b) a b. symbol xor (a b: ℕ): ℕ ≔ bitwise (xorb) (max a b) a b; notation xor infix 10; symbol testbit (a n: ℕ) : 𝔹; @@ -2243,6 +2234,7 @@ assume a; } } end; + // Strong (course-of-values) induction opaque symbol ind_ℕ_strong (p : ℕ → Prop) : diff --git a/Z.lp b/Z.lp index e9350ca..84187e1 100644 --- a/Z.lp +++ b/Z.lp @@ -176,8 +176,6 @@ end; symbol + : ℤ → ℤ → ℤ; notation + infix right 20; -builtin "+" ≔ +; - rule Z0 + $y ↪ $y with Zpos $x + Z0 ↪ Zpos $x with Zneg $x + Z0 ↪ Zneg $x @@ -273,8 +271,6 @@ symbol - x y ≔ x + — y; notation - infix left 20; -builtin "-" ≔ —; - opaque symbol -_same z : π (z + — z = Z0) ≔ begin induction @@ -401,28 +397,9 @@ begin refine g2 end; - - // Multiplication -symbol * : ℤ → ℤ → ℤ; -notation * infix right 22; - -builtin "*" ≔ *; - -// enable parsing of integers in decimal notation - -builtin "0" ≔ Z0; -builtin "1" ≔ _1; -builtin "2" ≔ _2; -builtin "3" ≔ _3; -builtin "4" ≔ _4; -builtin "5" ≔ _5; -builtin "6" ≔ _6; -builtin "7" ≔ _7; -builtin "8" ≔ _8; -builtin "9" ≔ _9; -builtin "10" ≔ _10; +symbol * : ℤ → ℤ → ℤ; notation * infix right 22; rule Z0 * _ ↪ Z0 with _ * Z0 ↪ Z0 @@ -431,7 +408,6 @@ with Zpos $x * Zneg $y ↪ Zneg (mul $x $y) with Zneg $x * Zpos $y ↪ Zneg (mul $x $y) with Zneg $x * Zneg $y ↪ Zpos (mul $x $y); - opaque symbol *_com x y : π (x * y = y * x) ≔ begin induction @@ -535,7 +511,6 @@ begin refine e end; - opaque symbol mul_distr_sub_pos_l (a x y : ℙ) : π (Zpos a * sub x y = sub (mul a x) (mul a y)) ≔ begin @@ -558,7 +533,6 @@ begin refine e end; - opaque symbol *_distr_l (z x y : ℤ) : π (z * (x + y) = z * x + z * y) ≔ begin induction @@ -614,7 +588,22 @@ begin { assume a; induction { reflexivity } { reflexivity } { reflexivity } } end; +// enable parsing of integers in decimal notation +builtin "0" ≔ Z0; +builtin "1" ≔ _1; +builtin "2" ≔ _2; +builtin "3" ≔ _3; +builtin "4" ≔ _4; +builtin "5" ≔ _5; +builtin "6" ≔ _6; +builtin "7" ≔ _7; +builtin "8" ≔ _8; +builtin "9" ≔ _9; +builtin "10" ≔ _10; +builtin "+" ≔ +; +builtin "*" ≔ *; +builtin "-" ≔ —; // Exponentiation @@ -630,7 +619,6 @@ rule _ ^ Z0 ↪ Zpos H with $x ^ (Zpos $p) ↪ power_pos $x $p with _ ^ (Zneg _) ↪ Z0; - // Comparison of integers require open Stdlib.Comp;