I got LEAN to recognize my proof that the identity function on the natural numbers is strictly increasing. Which is a very obvious statement, and I’m guessing there is an even shorter proof than the one I came up with
theorem id_nat_strinc : my_strinc id :=
assume n m : nat,
assume h : (n < m),
have h_1 : (n = id n), from refl n,
have h_2 : (m = id m), from refl m,
calc
(id n) = n : eq.symm h_1
... < m : h
... = id m : eq.symm h_2
), probably using some tactic that I don’t know the name of yet.
And now, this is a bit silly, but I’m having a little trouble finding a concise way to prove 3 < 5 in a way that LEAN recognizes.
Like, I think I could use the line of reasoning “3 is less than 3 + 1 (by lt_succ_of_le and le_refl), and 3 + 1 is less than 3 + 1 + 1 (by the same reason), so by transitivity of less than , 3 is less than 3+1+1, and 3+1+1 is 5, so 3 is less than 5”, but I would hope that there is some tactic where I can just say “hey, prove that 3 < 5 for me”, and it would say “yup, 3 is less than 5”. I’m guessing there probably is one, and I just don’t know the name of it.
If you happen to know the name of a tactic in LEAN where I just make a sufficiently obvious statement (such as 3 < 5) and it automatically finds a proof, please let me know.
Anyway, after I do that, my next steps are to prove that the composition of two strictly increasing functions from nat to nat is a strictly increasing from nat to nat, and to prove that the sum of two strictly increasing functions from nat to nat is a strictly increasing function from nat to nat.
Also maybe switch to using (non strictly) monotonically increasing, instead of strictly increasing.
Then after that idk, I’m just messing around mostly. It might be fun/neat to formalize some basic “first quarter econ supply and demand curves, but with general monotonic increasing and monotonic decreasing functions instead of straight lines” stuff.
