Implement my standard GCD program in Lean and it's so nice yay

Changes

2 changed files (+33/-0)

• Main.lean
  • @@ -59,3 +59,22 @@ theorem lsb_le_i (i : Nat) : lsb i ≤ i := by
    lsb i = 2 * lsb (i / 2) := by rw [lsb]; simp [h₁, h₂] _ ≤ 2 * (i / 2) := by simp [lsb_le_i (i / 2)] _ ≤ i := by exact Nat.mul_div_le i 2; + + + #check fun (α β γ : Type) (g : β → γ) (f : α → β) (x : α) => g (f x) + + + universe u + def ident {α : Type u} (x : α) := x + + + #check @ident + + #print lsb_le_i + + open Classical + + theorem dne {p : Prop} (h : ¬¬p) : p := + Or.elim (Classical.em p) + (fun hp : p => hp) + (fun hnp : ¬p => absurd hnp h)
• gcd.lean (new)
  • @@ -0,0 +1,14 @@
    + def gcd(a b : Nat) : Nat := + if b > 0 then gcd b (a % b) else a + termination_by b + decreasing_by + rename_i h + exact Nat.mod_lt a h + + #eval "test" + + def N := 1000 + + def A := List.range N + + #eval (A.map λ x => (A.map λ y => gcd x y).sum).sum