Random useless trash

Changes

1 changed files (+74/-0)

• Rec.lean (new)
  • @@ -0,0 +1,74 @@
    + import Mathlib + + -- example [Monoid S] (h₁ : ∀ x : S, e₁ * x = x ∧ x * e₁ = x) (h₂ : ∀ x : S, e₂ * x = x ∧ x * e₂ = x) : e₁ = e₂ := by + -- grind [h₁ e₂] + + + def g : Bool → ℕ + | true => 0 + | false => 1 + + #print g + + #check Bool.rec (motive := fun _ ↦ ℕ) 0 1 + + noncomputable def g'' := Bool.rec (motive := fun _ ↦ ℕ) 0 1 + + example : g'' true = 1 := by decide + + #check fun t ↦ Bool.recOn (motive := fun _ ↦ ℕ) t 0 1 + + -- noncomputable def g' t := Bool.recOn (motive := fun _ ↦ ℕ) t 0 1 + + + #check List.rec + + #check List.brecOn + + def len : List α → ℕ + | [] => 0 + | _ :: xs => 1 + len xs + + #print len + + noncomputable def len' (x : List α) : ℕ := + List.rec (motive := fun _ ↦ ℕ) 0 (fun _ _ l ↦ 1 + l) x + + #simp [len'] len' [1, 2, 3] + + example : len' [1, 2, 3] = 3 := by decide + + + -- def len2.{u_1} : {α : Type u_1} → List α → ℕ := + -- fun {α} x ↦ + -- List.brecOn x fun x f ↦ + -- (match (motive := (x : List α) → List.below x → ℕ) x with + -- | [] => fun x ↦ 0 + -- | head :: xs => fun x ↦ 1 + x.1) + -- f + + + #check Lean.trustCompiler + + + -- https://www.joachim-breitner.de/blog/817-F91_in_Lean + + def f91 (n : ℕ) : Option ℕ := + if n > 100 then + pure (n - 10) + else + f91 (n + 11) >>= f91 + partial_fixpoint + + theorem f91_spec_high (n : Nat) (h : 100 < n) : f91 n = some (n - 10) := by + unfold f91 + grind + + theorem f91_spec_low (n : Nat) (h₂ : n ≤ 100) : f91 n = some 91 := by + unfold f91 + + theorem f91_spec (n : Nat) : f91 n = some (if n ≤ 100 then 91 else n - 10) := by + + + theorem f91_total (n : Nat) : (f91 n).isSome := by + grind