Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

compound repeat first tactic no longer solves all three permutations of \and propositions #121

Open
jordane95 opened this issue Jul 7, 2024 · 0 comments

Comments

@jordane95
Copy link

The tactics chapter states that

In the first example, the left branch succeeds, whereas in the second one, it is the right one that succeeds.
In the next three examples, the same compound tactic succeeds in each case:

example (p q r : Prop) (hp : p) : p ∨ q ∨ r :=
  by repeat (first | apply Or.inl; assumption | apply Or.inr | assumption)

example (p q r : Prop) (hq : q) : p ∨ q ∨ r :=
  by repeat (first | apply Or.inl; assumption | apply Or.inr | assumption)

example (p q r : Prop) (hr : r) : p ∨ q ∨ r :=
  by repeat (first | apply Or.inl; assumption | apply Or.inr | assumption)

The tactic tries to solve the left disjunct immediately by assumption;
if that fails, it tries to focus on the right disjunct; and if that
doesn't work, it invokes the assumption tactic.

However, running it locally cannot solve all the subgoals.
Here is the state left unsolved

example (p q r : Prop) (hq : q) : p ∨ q ∨ r :=
  /-
  case h
  p q r : Prop
  hq : q
  ⊢ q ∨ r
  -/
  by repeat (first | apply Or.inl; assumption | apply Or.inr | assumption)
@jordane95 jordane95 changed the title compound repeat first tactic no longer solves all three permutations of \and propositions compound repeat first tactic no longer solves all three permutations of \and propositions Jul 7, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant