tactic noobie

Stream: general

[Johan Commelin]

I'm taking a stab at the tfae tactic. This is what I have so far:

meta def tfae_have
  (p₁ : parse small_nat)
  (re : parse (((tk "→" <|> tk "->") *> return tt) <|> ((tk "↔" <|> tk "<->") *> return ff)))
  (p₂ : parse small_nat)
  (discharger : tactic unit :=
    (solve_by_elim <|> tauto <|> using_smt (smt_tactic.intros >> smt_tactic.solve_goals))) :
  tactic unit := do
    g <- get_goals,

Now I would like to loop over my goals, and check if any of them has the form tfae [P, Q, ..., bla]. How do I do that?

[Reid Barton]

maybe we can cocalc this?

[Johan Commelin]

Sure!

[Johan Commelin]

Just in the big project?

[Reid Barton]

Seems easiest

[Johan Commelin]

I'm there

[Reid Barton]

Maybe working on the main goal (target) is good enough. I'm looking at the split_ifs code and that is what it does

[Reid Barton]

I think this is going to need the tfae stuff to be defined already