Grace/Core/Nat/Order.g17

Open in Workbench Download source

Imports

Grace.Core.Nat.Algebra

Declarations

• LessEqual predicate
• Less predicate
• LessEqual.reflexive theorem derivation
• LessEqual.zero theorem derivation
• LessEqual.add_right theorem derivation
• LessEqual.successor theorem derivation
• LessEqual.transitive theorem derivation
• LessEqual.add_monotone_right theorem derivation
• Less.implies_LessEqual theorem derivation
• LessEqual.natural_right theorem derivation
• Less.natural_right theorem derivation

Source

1-- Natural-number order2-- Part of the Grace17 proof assistant for mathematics based on set theory.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Core.Nat.Order8namespace Grace.Core.Nat.Order9import Grace.Core.Nat.Algebra10export open Grace.Core.Nat.Order1112predicate LessEqual (a b : Nat) := exists k, Nat(k) and add(a, k) = b13notation infix 50 "≤" => LessEqual for Nat14notation infix 50 "<=" => LessEqual for Nat15notation infix 50 "≥" => reverse LessEqual for Nat16notation infix 50 ">=" => reverse LessEqual for Nat1718predicate Less (a b : Nat) := succ(a) ≤ b19notation infix 50 "<" => Less for Nat20notation infix 50 ">" => reverse Less2122theorem LessEqual.reflexive (a : Nat)23  shows a ≤ a24proof25  simp [LessEqual, Naturals.constructor.zero, add.right_unit]2627theorem LessEqual.zero (b : Nat)28  shows 0 ≤ b29proof30  witness b31  simp [add]3233theorem LessEqual.add_right (a k : Nat)34  shows a ≤ add(a, k)35proof36  witness k37  reflexivity3839theorem LessEqual.successor (a : Nat)40  shows a ≤ succ(a)41proof42  witness 143  simp [Naturals.constructor.zero, Naturals.constructor.succ]44  simp [add.succ_right, add.right_unit]4546theorem LessEqual.transitive (a b c : Nat)47  requires hab : a ≤ b48  requires hbc : b ≤ c49  shows a ≤ c50proof51  obtain ⟨k, hk⟩ := hab52  obtain ⟨l, hl⟩ := hbc53  witness add(k, l)54  simp [add.closed]55  simp [add.associative_reverse]5657theorem LessEqual.add_monotone_right (a b c : Nat)58  requires hab : a ≤ b59  shows add(a, c) ≤ add(b, c)60proof61  obtain ⟨k, hk⟩ := hab62  witness k63  simp64  simp [add.associative, add.swap, add.commutative]6566theorem Less.implies_LessEqual (a b : Nat)67  requires hab : a < b68  shows a ≤ b69proof70  obtain ⟨k, hk⟩ := hab71  witness succ(k)72  simp [Naturals.constructor.succ]73  simp [add.successor_shift]7475-- The right side of a bound whose left side is a natural number is one too:76-- the arithmetic tactics type an opaque bounded term from these.77theorem LessEqual.natural_right (a : Nat, b : Set)78  requires hab : a ≤ b79  shows Nat(b)80proof81  obtain ⟨k, hk, sum⟩ := hab82  rw ← sum83  exact add.closed at k, a8485theorem Less.natural_right (a : Nat, b : Set)86  requires hab : a < b87  shows Nat(b)88proof89  have natSucc : Nat(succ(a)) by simp [Naturals.constructor.succ]90  exact LessEqual.natural_right at succ(a), b with natSucc, hab9192end Grace.Core.Nat.Order93