generated names

Stream: new members

[Callan McGill]

I am going through kevin buzzard's very pleasant current undergraduate course and there is a proof of the form:

example : ((P ∧ Q) ∧ R) ↔ (P ∧ (Q ∧ R)) :=
begin
  sorry
end

I know a bit about coq style proofs and so I wanted to do this using semicolons as something like:

example : ((P ∧ Q) ∧ R) ↔ (P ∧ (Q ∧ R)) :=
begin
  split; intros, cases 1, cases 1; try cases 1; cases 2; split; try assumption; split; try assumption
end

or something like that, but I don't know what names lean is guaranteed to generate so I wanted to know what is the proper way to refer to such names in a robust way?

[Kevin Buzzard]

This works:

import tactic

variables (P Q R : Prop)

example : ((P ∧ Q) ∧ R) ↔ (P ∧ (Q ∧ R)) :=
begin
  split;
  { intro h,
    cases h with h1 h2,
    try {cases h1},
    try {cases h2},
    split;
    try {assumption},
    split;
    assumption,
  },
end

I don't know how to run cases on a term whose name I don't know.

[Kyle Miller]

tactic#destruct seems useful here

example {P Q R : Prop} : ((P ∧ Q) ∧ R) ↔ (P ∧ (Q ∧ R)) :=
begin
  split;
  repeat { intro h, try { destruct h }, };
  repeat { split };
  assumption,
end

[Kyle Miller]

It seems to be like cases, but it does tactic#revert to all the new hypotheses