how to find all the different proofs of one proposition?

Stream: new members

[chenjulang]

how to find all the different proofs of one proposition?Like this proposition, we have two ways to prove, but how to find? :
example : {1, 2} ∪ {2, 4} = {1, 2, 4} := by
ext n
dsimp
constructor
· intro h
obtain (h | h) | (h | h) := h
· left
apply h
· right
left
apply h
-- and much, much more
· sorry
· sorry
· sorry
但还有更好的方法：这是纯粹的命题逻辑，该策略tauto（参见 示例 8.1.8）就是针对这种情况而设计的。

example : {2, 1} ∪ {2, 4} = {1, 2, 4} := by
ext n
dsimp
tauto

[Ruben Van de Velde]

Please check out #backticks

[chenjulang]

example : {1, 2} ∪ {2, 4} = {1, 2, 4} := by
  ext n
  dsimp
  constructor
  · intro h
    obtain (h | h) | (h | h) := h
    · left
      apply h
    · right
      left
      apply h
  -- and much, much more
    · sorry
    · sorry
  · sorry


example : {2, 1} ∪ {2, 4} = {1, 2, 4} := by
  ext n
  dsimp
  tauto

[chenjulang]

This question has two ways to prove like the above.

But how do we find different proofs of any other problems ?

[chenjulang]

For Students , more ways to prove a new problem , is better for them to understand or fall in love with maths. Right?

[Kevin Buzzard]

I think an algorithm to find all proofs of something is even harder to make than an algorithm which finds one proof of something, and this easier algorithm is already out of reach in practice.

[Gareth Ma]

chenjulang said:

For Students , more ways to prove a new problem , is better for them to understand or fall in love with maths. Right?

This problem of "finding new / all (whatever that means) proofs for a problem" is hard even in normal maths. We constantly discover new proofs for classical problems, so it's the same in Lean too.

However for your original question, you probably mean how to find the tactics ext n ; dsimp ; tauto. Apart from the obvious answer "write more code and read more code", there is a tactic called hint that was implemented very recently. It is meant to do exactly what you want - propose suggestions to close goals. For example, in your case:

example : {2, 1} ∪ {2, 4} = ({1, 2, 4} : Finset ℕ) := by
  hint

/-
Try these:
• decide
-/

Actually gives you a one-liner instead of your 3-liner :)

[chenjulang]

Gareth Ma said:

chenjulang said:

For Students , more ways to prove a new problem , is better for them to understand or fall in love with maths. Right?

This problem of "finding new / all (whatever that means) proofs for a problem" is hard even in normal maths. We constantly discover new proofs for classical problems, so it's the same in Lean too.

However for your original question, you probably mean how to find the tactics ext n ; dsimp ; tauto. Apart from the obvious answer "write more code and read more code", there is a tactic called hint that was implemented very recently. It is meant to do exactly what you want - propose suggestions to close goals. For example, in your case:

example : {2, 1} ∪ {2, 4} = ({1, 2, 4} : Finset ℕ) := by
  hint

/-
Try these:
• decide
-/

Actually gives you a one-liner instead of your 3-liner :)

thanks！Benefited a lot！