2
$\begingroup$

I can use 'subst' to prove that if a=b and a is positive then b is positive:

example (a b : Peano) (h1 : a = b) (h2 : pos a) : pos b := Eq.subst h1 h2

How do I prove that if a=b and a > c then b > c:

example (a b c: Peano) (h1 : a = b) (h2 : gt a c) : gt b c := Eq.subst h1 h2 -- does not work

Note that I am learning Lean 4 by using my own 'Peano' natural numbers, so I only want a solution that uses non-numeric tactics (i.e. propositional logic and equality). It appears that 'congr' or 'congrArg' may help (do I need to specify a lambda expression?) but I have not succeeded.

$\endgroup$
1
  • $\begingroup$ Note, Lean isn't based on propositional logic or first-order logic, so some things which you would consider pure logical rules in first-order logic, like substitution, are actually theorems proved in Lean via induction on the definition of equality. At the heart of Lean is the rec recursor. Then match, induction, etc are built on top of that to make case analysis and induction easier. For equality specifically, the ▸ macro, rewrite tactic. and calc proofs are designed to make it easy for users. And then there is even more powerful automation like the simp tactic on top of that. $\endgroup$
    – Jason Rute
    Jan 4 at 12:51

1 Answer 1

1
$\begingroup$

I recommend the ▸ macro, which you can write using \t in VSCode.

-- definitions of Peano and gt don't matter here
axiom Peano : Type  
axiom gt (a b : Peano): Prop

example (a b c : Peano) (h1 : a = b) (h2 : gt a c) : gt b c :=
  h1 ▸ h2

The macro is quite flexible and can be used in a number of situations where you want to do substitution using an equality.

As for the more direct approach, I'm not sure why Eq.subst h1 h2 doesn't work, but if you fill in all the implicit arguments it works:

example (a b c : Peano) (h1 : a = b) (h2 : gt a c) : gt b c :=
  @Eq.subst Peano (fun x => gt x c) a b h1 h2

If you are fine with the rewrite tactic (which is a purely logical tactic), then that works well also:

example (a b c : Peano) (h1 : a = b) (h2 : gt a c) : gt b c := by
  rewrite [<- h1]
  exact h2

As for learning how equality actually works in Lean, I highly recommend you read the Equality section in Theorem Proving in Lean 4.

In particular, equality is defined inductively (just like the natural numbers) with one constructor refl. You can even define your own version:

inductive MyEq : α → α → Prop where
  | refl (a : α) : MyEq a a

Since it is an inductive, we can use induction (sometimes called "path induction"):

example (a b c : Peano) (h1 : MyEq a b) (h2 : gt a c) : gt b c := by 
  induction h1
  exact h2

The idea is that if we can construct or prove P a and we have MyEq a b, then we can construct or prove P b as well.

This is also easy to write as a case analysis using the single refl constructor for MyEq.

example (a b c : Peano) (h1 : MyEq a b) (h2 : gt a c) : gt b c :=
  match h1 with
  | MyEq.refl a => h2

Finally, if you really want to get to the very inner guts of Lean, you can directly use the rec recursor (which I don't recommend for actual Lean code, but in this case, it is really simple to use).

example (a b c : Peano) (h1 : MyEq a b) (h2 : gt a c) : gt b c :=
  MyEq.rec h2 h1
$\endgroup$
1
  • $\begingroup$ Many thanks for your detailed and extremely helpful answers! I used the simple "rw [h]; exact" to finally prove: x > y ∧ pos z → x * z > y * z (together with some previously proved theorems). $\endgroup$ Jan 4 at 15:11

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.