TFAE

Stream: general

[Reid Barton]

What's the best way to structure the statement and proof when I want to prove (1), (2), and (3) are equivalent by showing (1) => (2) => (3) => (1)?

[Reid Barton]

Let's say (1) is the definition of something, and (2) and (3) are alternate definitions and I'd like to end up with (1) <=> (2) and (1) <=> (3).
I could just do something very straightforward (prove (1) => (2), (2) => (3), (3) => (1) as separate top-level lemmas, then conclude (1) <=> (2) and (1) <=> (3) manually) but maybe there is a better idea.

[Keeley Hoek]

it'd be cool if there was a tactic for this

[Mario Carneiro]

I'm not sure how a tactic could help. The problem is the proof structuring, you don't want all three major parts to be in one big proof

[Mario Carneiro]

It is easy enough to encode the idea of a cycle in a preorder, and deduce equivalence of all parts, which you could prove once and for all and apply as a theorem for your 11-part theorem

[Mario Carneiro]

For the case of 2 or 3 statements, it's easier just to use the lemmas as given

[Mario Carneiro]

I'm not sure I've ever had a case of 4+ statements proven in cyclic order where I actually care about all 4 equivalences

[Keeley Hoek]

I was just thinking of a tactic which turns a single goal "a iff b iff c iff d iff ..." into a cyclic set of goals "a=>b", "b=>c", etc. Probably itd be too yuck for anything big?

[Mario Carneiro]

There are two problems with that: (1) the goals might be big - if they aren't there isn't really a need for this (2) The output is a iff b iff c - what is that? If it is a big conjunction then there is still work to be done to make a usable lemma

[Keeley Hoek]

yep ok sure

[Reid Barton]

(2) The output is a iff b iff c - what is that? If it is a big conjunction then there is still work to be done to make a usable lemma

Yeah, this is where I really got stuck

[Chris Hughes]

Also a iff b iff c is not the same as a iff b and b iff c

[Reid Barton]

I guess one out-there idea is to define

def the_following_are_equivalent (ps : list Prop) := ∀ p q ∈ ps, p ↔ q

and then a helper function which extracts for a given pair of indices implication (or bi-implication) between the corresponding Props

[Reid Barton]

Mario I do agree that when the list is really long, typically some of the equivalent statements are not included for later use, but rather to elucidate the structure of the argument. Or to say: here is a variant definition of something and you might wonder whether it is equivalent to the official one; it is (and now we never need to talk about it again).

[Simon Hudon]

I could imagine a presentation like:

lemma my_interesting_equivalences :
   the_following_are_equivalent
    [ formula1,
      formula2,
      formula3 ] :=
begin
  circular_implication,
  { /- proof1 -/ },
  { /- proof2 -/ },
  { /- proof3 -/ },
end

and have circular_implication extract the two by two equivalences as separate lemmas: my_interesting_equivalences_1_2, my_interesting_equivalences_1_3, my_interesting_equivalences_2_3.

[Simon Hudon]

Or, even better:

lemma my_interesting_equivalences :
   the_following_are_equivalent
    [ Reids_defn ::= formula1,
      Simons_defn ::= formula2,
      Marios_defn ::= formula3 ] :=
begin
  circular_implication,
  { /- proof1 -/ },
  { /- proof2 -/ },
  { /- proof3 -/ },
end

and then have my_interesting_equivalences_Reids_defn_iff_Simons_defn etc and make Reids_defn, Simons_defn and Marios_defn into stand alone definitions.

[Mario Carneiro]

This won't work inside a theorem, you can't make new definitions

[Mario Carneiro]

Also, that's a quadratic number of generated lemmas

[Simon Hudon]

This won't work inside a theorem, you can't make new definitions

I'm fairly sure that you can.

[Simon Hudon]

Also, that's a quadratic number of generated lemmas

Yes it is but that's what you're trying to prove if you use this approach, no? You could also state only consecutive equivalences but I think that would make the use of those lemmas harder.

[Kenny Lau]

I know there's a tactic that can generate iff statements for any inductive type

[Mario Carneiro]

Here's how I think you can do it with just definitions:

import data.list.basic

namespace list

@[simp] def last' {α} : α → list α → α
| a []     := a
| a (b::l) := last' b l

def TFAE (l : list Prop) : Prop := ∀ x ∈ l, ∀ y ∈ l, x ↔ y

theorem TFAE_of_cycle {a b} {l : list Prop} :
  list.chain (→) a (b::l) → (last' b l → a) → TFAE (a::b::l) :=
sorry

def TFAE.out {l} (h : TFAE l) (n₁ n₂)
 (h₁ : n₁ < list.length l . tactic.exact_dec_trivial)
 (h₂ : n₂ < list.length l . tactic.exact_dec_trivial) :
  list.nth_le l n₁ h₁ ↔ list.nth_le l n₂ h₂ :=
h _ (list.nth_le_mem _ _ _) _ (list.nth_le_mem _ _ _)

theorem TFAE_test (x y : ℕ) : TFAE [true, x = x, y = y] :=
TFAE_of_cycle (by simp) (λ _, trivial)

example (x y : ℕ) : x = x ↔ y = y := (TFAE_test x y).out 1 2

end list

[Mario Carneiro]

A tactic could be used to unfold the definitions involved in TFAE_of_cycle

[Mario Carneiro]

then again, simp already does that

[Kenny Lau]

wow that's so magical

[Mario Carneiro]

Another option besides TFAE.out is to use

theorem TFAE_iff_iff {a l} : TFAE (a::l) ↔ ∀ b ∈ l, a ↔ b := sorry

as a simp lemma, that way you can simplify a TFAE into a bunch of iffs with the first thing in the list (which is usually what you will want to have as the output theorems)

[Cyril Cohen]

@Assia Mahboubi pointed this thread to me. It is funny because I was considering adding such a feature to mathcomp: https://github.com/math-comp/math-comp/commit/0d41046cff37af7b85da0e771e3d25a4c640edbf

[Patrick Massot]

What is the interface you chose then? It's hard to tell from the link without knowing Coq

[Cyril Cohen]

@Patrick Massot I chose something like: [↔ P0; ...; Pn] := (all_iff P0 [P1; ...; Pn]) := ((P0 → P1) ∧ (P1 → P2) ∧ ... ∧ (Pn → P0)) (pseudo syntax)
And the main theorem all_iffLR says roughly that [↔ P0; ...; Pn] → ∀i j, Pi → Pj (pseudo syntax again), and is a coercion to a function, so that a lemma mylemma : [↔ P0; ...; Pn] can be applied to natural numbers to give mylemma i j, a proof of Pi → Pj.

[Johan Commelin]

That looks like a really nice way to attack this.

[Johan Commelin]

As a mathematician I wonder if we could use tactics to allow for even more general ways of proving an all_iff instead of only cycles.

[Cyril Cohen]

One of the improvements I have in mind is to provide a graph. And have the computational part of the system check it is strongly connected, then ask to prove only the edges. (so no deep tactic involved, just reflexion)

[Johan Commelin]

Right.

[Johan Commelin]

But it would allow for more convenience.

[Cyril Cohen]

Yes

[Johan Commelin]

The interactive version would first ask the user to supply a graph. Then the system does the connectedness check (or asks the user for a proof). And then the tactic goes on to supply you all the edges 1-by-1

[Johan Commelin]

I mean, check this out: https://stacks.math.columbia.edu/tag/04GG

[Johan Commelin]

Too bad we don't have a lot about graphs in Lean.

[Cyril Cohen]

I would start my proof by applying the lemma all_iff_from [(2,1);(5,3)...](implicit arguments + unification would do the job of checking the connectedness of the graph, and a split would ask for all the implications, that is why I see no need for a tactic...

[Cyril Cohen]

And since we have graphs in coq with math-comp, I am really eager to try :)

[Johan Commelin]

But do you have henselian local rings?

[Johan Commelin]

Just kidding...

[Johan Commelin]

I would love to have this kind of stuff in Lean!

[Johan Commelin]

How hard is the connectedness check? I guess that shouldn't be too hard, right?

[Cyril Cohen]

it is just a dfs

[Johan Commelin]

/me walks over to his copy of TAOCP

[Johan Commelin]

Right, and you need to generate a proof along the way.

[Johan Commelin]

(I've never really written tactics before... so I'm just thinking out loud.)

[Johan Commelin]

Hmmm... but most of this isn't even meta.

[Johan Commelin]

@Cyril Cohen Two questions: (1) Do you have any experience in Lean? (2) Where can we find your coq implementation?

[Cyril Cohen]

@Johan Commelin (1) I only saw @Mario Carneiro and @Johannes Hölzl in action, I have no more experience than that. (2) my current coq implementation does not support graphs yet, only what I described in the message you replied to and it is here: https://github.com/math-comp/math-comp/commit/0d41046cff37af7b85da0e771e3d25a4c640edbf (waiting patiently to be cleaned and merged since august)

[Johan Commelin]

Ok, understood :thumbs_up:

[Patrick Massot]

Nice! So the current implementation in Coq is about using a chain of equivalences, not proving it. But clearly both ways are useful. I'm sure we'll soon have this in Lean

[Cyril Cohen]

@Patrick Massot it's also about proving it, but only from circular implications P0 -> ... -> Pn -> P0 (no arbitrary strongly connected graph)

[Patrick Massot]

ok, nice

[Patrick Massot]

I guess it already covers most use cases, you only need to list the conditions in the order you intend to prove the chain of implications, and then you can use any implication

[Johan Commelin]

import data.vector

@[pattern] def vector.mk {α : Type*} {n : ℕ} (l : list α) (pr : l.length = n) :
  vector α n := ⟨l, pr⟩

def all_iff : ∀ {n : ℕ}, vector Prop n → Prop
| 0     Ps := true
| 1     Ps := Ps.head
| (n+2) Ps := (Ps.head → Ps.tail.head) ∧ (all_iff Ps.tail)

local notation `[↔` l:(foldr `, ` (h t, list.cons h t) list.nil `]`) :=
  all_iff (vector.mk l rfl)

example : [↔ true, false] := sorry

def all_iff_LR {n : ℕ} {Ps : vector Prop n} (H : all_iff Ps) : ∀ (i j : fin n), Ps.nth i → Ps.nth j :=
begin
  sorry
end

[Johan Commelin]

Oops, there is a bug. I'm not closing the cycle.

[Reid Barton]

Somewhere on Twitch there is now a video of me having proved 1 => 2 and 2 => 3 and 3 => 1 and then taking several minutes to figure out how to prove 2 <=> 1 and 3 <=> 1 and then later being unable to remember whether I had proved 2 <=> 1 or 1 <=> 2. So I guess there is some real non-zero value to this.

[Johan Commelin]

This is better:

import tactic.interactive
import data.vector

@[pattern] def vector.mk {α : Type*} {n : ℕ} (l : list α) (pr : l.length = n) :
  vector α n := ⟨l, pr⟩

@[reducible] def all_iff' : Prop → list Prop → Prop
| P₀ []               := true
| P₀ (P₁ :: [])       := P₁ → P₀
| P₀ (P₁ :: P₂ :: Ps) := (P₁ → P₂) ∧ all_iff' P₀ (P₂ :: Ps)

def all_iff {n : ℕ} : vector Prop n → Prop
| ⟨[],             h⟩ := true
| ⟨P :: [],        h⟩ := true
| ⟨P₀ :: P₁ :: Ps, h⟩ := (P₀ → P₁) ∧ all_iff' P₀ (P₁ :: Ps)

local notation `[↔` l:(foldr `, ` (h t, list.cons h t) list.nil `]`) :=
  all_iff (vector.mk l rfl)

example : [↔ true, true, true] :=
begin
  split, tauto,
  dsimp [all_iff'], tauto
end

[Johan Commelin]

I would like to not have the dsimp [all_iff'] in the example. I marked the definition reducible, but that didn't help.

[Reid Barton]

I don't know whether this matters here, but when I was playing around with this stuff I found you can also do

local notation `[↔` p0 `, ` l:(foldr `, ` (h t, list.cons h t) list.nil `]`) :=
  all_iff (vector.mk (p0 :: l) rfl)

[Reid Barton]

which lets you guarantee that the list is nonempty

[Johan Commelin]

I'm not sure if we want that guarantee... for interaction sure. But maybe this code will also be used in automation or something. And then it would be nice if [] is not a problem.

[Reid Barton]

If you dsimp only [all_iff, all_iff', vector.mk] first then you get a conjunction of the 3 iffs

[Reid Barton]

I thought it might be more likely that allowing [] is a problem for automation than that disallowing it is a problem. But I'm not sure either, just thought I would mention the possibility.

[Reid Barton]

I think a very simple tactic which turns an all_iff goal with list of length N into N subgoals (or possibly a conjunction of N implications) will probably be useful. Otherwise, I think it will be hard to avoid making the intermediate goals confusing.

[Johan Commelin]

True, something like that is necessary.

[Johan Commelin]

@Cyril Cohen I am very bad at reading coq code, apparently...

[Johan Commelin]

I'm trying to prove all_iff_LR in Lean. I'm exploding into different cases. Is there a good strategy to prove this by induction?

[Johan Commelin]

Do you case on i < j or something similar?

[Cyril Cohen]

@Johan Commelin I am using a lemma saying (roughly) that a function f : nat -> T respects the order (< for nat, and an arbitrary order on T (-> on Prop in our case)) if one can prove that f i < f (i + 1) (or f i -> f (i + 1) in our case). Only then, I do an induction.

[Johan Commelin]

Hmm, I see. That seems smart.

[Johan Commelin]

So now I need to find that lemma in mathlib. @Kenny Lau Do you know the function that Cyril is talking about?

[Kenny Lau]

is it even in mathlib?

[Kenny Lau]

I'd just use induction to prove it

[Johan Commelin]

Dunno.

[Johan Commelin]

lemma foobar {X : Type*} [preorder X] (f : ℕ → X) : monotone f ↔ ∀ i, f i ≤ f (i+1) :=
begin
  split,
  { intros h i, exact h (nat.le_succ i) },
  { intro H,
    unfold monotone,
    intros a b h,
    induction h with x h ih,
    { refl },
    { exact le_trans ih (H x) }
  }
end

[Johan Commelin]

It still needs a name and golfing (-;

[Johan Commelin]

Ok, I'm making slow progress. I'll try to post something later tonight.

[Johan Commelin]

@Scott Morrison @Keeley Hoek I think I found a missing feature in tidy. It doesn't split \iff in the assumptions into two implications. If it did, I guess it could have solved more of my goals.

[Keeley Hoek]

@Johan Commelin Could you give me an example? In the (admittedly baby) example

constants a b : Prop

def lol : iff a b := begin
  tidy,
  admit
end

tidy does do what you're saying, I think.

[Keeley Hoek]

Or are you talking about tidy not converting iff hypotheses into a pair of implies hypotheses? Maybe it should do that...

[Keeley Hoek]

For the latter, give https://github.com/leanprover/mathlib/pull/344 (i.e. https://github.com/leanprover-community/mathlib/tree/auto-cases-iff) a try.

[Johan Commelin]

@Keeley Hoek Cool! That kills of another goal (-;

[Mario Carneiro]

What was wrong with the sketch I gave earlier for TFAE_of_cycle? It should be isomorphic to cyril's definition

[Keeley Hoek]

that list.chain syntax is sick Mario

[Mario Carneiro]

Here's the whole proof:

namespace list

@[simp] def last' {α} : α → list α → α
| a []     := a
| a (b::l) := last' b l

theorem last'_mem {α} : ∀ a l, @last' α a l ∈ a :: l
| a []     := or.inl rfl
| a (b::l) := or.inr (last'_mem b l)

def TFAE (l : list Prop) : Prop := ∀ x ∈ l, ∀ y ∈ l, x ↔ y

theorem TFAE_nil : TFAE [] := forall_mem_nil _
theorem TFAE_singleton (p) : TFAE [p] := by simp [TFAE]

theorem TFAE_cons_of_mem {a b} {l : list Prop} (h : b ∈ l) :
  TFAE (a::l) ↔ (a ↔ b) ∧ TFAE l :=
⟨λ H, ⟨H a (by simp) b (or.inr h), λ p hp q hq, H _ (or.inr hp) _ (or.inr hq)⟩,
 begin
   rintro ⟨ab, H⟩ p (rfl | hp) q (rfl | hq),
   { refl },
   { exact ab.trans (H _ h _ hq) },
   { exact (ab.trans (H _ h _ hp)).symm },
   { exact H _ hp _ hq }
 end⟩

theorem TFAE_cons_cons {a b} {l : list Prop} : TFAE (a::b::l) ↔ (a ↔ b) ∧ TFAE (b::l) :=
TFAE_cons_of_mem (or.inl rfl)

theorem TFAE_of_cycle {a b} {l : list Prop} :
  list.chain (→) a (b::l) → (last' b l → a) → TFAE (a::b::l) :=
begin
  induction l with c l IH generalizing a b; simp [TFAE_cons_cons, TFAE_singleton] at *,
  { exact iff.intro },
  intros ab bc ch la,
  have := IH bc ch (ab ∘ la),
  exact ⟨⟨ab, la ∘ (this.2 c (or.inl rfl) _ (last'_mem _ _)).1 ∘ bc⟩, this⟩
end

theorem TFAE.out {l} (h : TFAE l) (n₁ n₂)
 (h₁ : n₁ < list.length l . tactic.exact_dec_trivial)
 (h₂ : n₂ < list.length l . tactic.exact_dec_trivial) :
  list.nth_le l n₁ h₁ ↔ list.nth_le l n₂ h₂ :=
h _ (list.nth_le_mem _ _ _) _ (list.nth_le_mem _ _ _)

theorem TFAE_test (x y : ℕ) : TFAE [true, x = x, y = y] :=
TFAE_of_cycle (by simp) (λ _, trivial)

example (x y : ℕ) : x = x ↔ y = y := (TFAE_test x y).out 1 2

end list

[Mario Carneiro]

There is a theorem that says that you can put a list.chain together over a transitive relation, but I had to prove the rest by induction anyway so it wasn't necessary

[Johan Commelin]

@Mario Carneiro I think the only thing that was wrong with it was that I didn't understand what you were doing...

[Mario Carneiro]

list.chain says that you have forward implications along the list, last l -> a gives the final backward arrow

[Mario Carneiro]

and they are both defined naturally by recursion making the proofs easy

[Johan Commelin]

@Mario Carneiro Ok, so I was almost done with a slightly clunkier implementation. :lol:

[Johan Commelin]

Would you mind pushing your stuff to a tfae branch on community?

[Johan Commelin]

I think we should put everything into a tfae namespace.

[Mario Carneiro]

I would just put it all in list.basic

[Mario Carneiro]

and in the list namespace, as you can see

[Johan Commelin]

Ok, fine with me.

[Johan Commelin]

Do you want to capitalise TFAE?

[Mario Carneiro]

dunno, seemed nicer that way

[Mario Carneiro]

tfae could be misread?

[Johan Commelin]

Maybe. TFAE feels like shouting.

[Johan Commelin]

I wouldn't mind having tfae.

[Mario Carneiro]

it's always the way I see it on the blackboard

[Johan Commelin]

That is true. But on the blackboard I also see Lemma and Thm...

[Mario Carneiro]

I would also not have any notation. for me tfae [p, q, r] is sufficient

[Mario Carneiro]

[<-> p, q, r] doesn't seem to buy much

[Johan Commelin]

Right, I also came to that conclusion

[Johan Commelin]

It is even easier to read.

[Mario Carneiro]

(none of this is to cast aspersions on Cyril's work; the style and design decisions are different there)

[Johan Commelin]

If you push your stuff, I would like to see if I can do anything with tfae_of_graph.

[Johan Commelin]

Some how you need to show that the transitive closure of the relation that is your graph is everything. Would an auto_param be able to do that?

[Mario Carneiro]

you are talking about Cyril's extension? I wouldn't want to try that without using a tactic to guide the whole process

[Johan Commelin]

Why not?

[Mario Carneiro]

because the number of goals is very nonuniform

[Mario Carneiro]

the types are too complicated to get much help from lean

[Mario Carneiro]

again, this reflects a difference in design from Coq. It's easier to do strongly connected checking in the kernel in Coq

[Mario Carneiro]

in lean we would do it with a tactic

[Johan Commelin]

Pseudo-code:

lemma tfae_of_graph (Ps : list Prop) (G : list (fin n x fin n)) (H : proof_that_G_generates_everything)
(proofs : \forall (i,j) \in G, Ps i \implies Ps j) : tfae Ps

[Johan Commelin]

Ok, I agree that maybe the Lean way is to use tactics

[Mario Carneiro]

You would have to supply proofs manually which is not nice

[Johan Commelin]

I don't know anything about auto_params but I would definitely want H to be automated by some tactic.

[Johan Commelin]

Right, so proofs better be a list of mvars, is that what you mean?

[Patrick Massot]

this would not be interactive because of the proofs parameter

[Johan Commelin]

Well, if you apply it, you would then be left with a goal that asks for proofs.

[Mario Carneiro]

Here's a conjecture: Given any SC graph on 1...n, there is a way to connect 1-2, 2-3, ..., n-1 by disjoint paths in the graph

[Johan Commelin]

And you would want to split that into a bunch of goals.

[Johan Commelin]

What is SC?

[Mario Carneiro]

strongly connected

[Johan Commelin]

I see.

[Mario Carneiro]

if true, the generalization is always redundant

[Mario Carneiro]

if you supply 1<->2 and 2<->3 then you have four proofs, and you could have just composed the proofs 3->2 and 2->1 to get a result in the form for tfae_of_cycle

[Johan Commelin]

Here is a graph: 1 -> 3 -> 2 -> 1

[Mario Carneiro]

of course

[Johan Commelin]

Did I misunderstand your conjecture?

[Mario Carneiro]

so I guess we need a theorem about permuting the graph

[Mario Carneiro]

no, that's a counterexample

[Johan Commelin]

I'dd just do a meta dfs

[Mario Carneiro]

new conjecture: there is a way to permute the vertices so that the first conjecture holds

[Johan Commelin]

That is trivial

[Mario Carneiro]

is it?

[Johan Commelin]

Hmm, maybe not.

[Johan Commelin]

But, why do you not want to reuse edges?

[Mario Carneiro]

because that way you can achieve the same with a straight line proof where you inline the relevant parts in each subproof

[Mario Carneiro]

i.e. the proof 3->2 only appears as part of the proof 3->1 in my example

[Mario Carneiro]

so it doesn't need to be stored and reused

[Johan Commelin]

Here is another graph: 1 -> 2 -> 3 -> 1; 2 -> 4 -> 1; 2 -> 5 -> 1

[Mario Carneiro]

foiled again

[Johan Commelin]

Hmm, you don't even need vertex 5.

[Mario Carneiro]

okay so we definitely need a tactic to manage this kind of structure

[Johan Commelin]

So the tactic takes a graph as input, and then proves that it is SC, and generates a list of goals, right?

[Mario Carneiro]

yes

[Reid Barton]

it might be worth considering the aforementioned https://stacks.math.columbia.edu/tag/04GG when imagining what the UI might look like

[Patrick Massot]

Do we really want the tactic to decide on a list of implications to prove? Sometimes there will be several solutions, some easier than others

[Johan Commelin]

No, you provide a list of edges.

[Johan Commelin]

You get to prove those. And the tactic shows that this is enough.

[Patrick Massot]

ok, I prefer that

[Reid Barton]

for example, listing all the edges and then, separately, all the proofs might be less nice than being able to interleave them

[Mario Carneiro]

My suggestion: suppose the goal is tfae [p1, p2, p3, p4, p5], then you can call tfae [1 -> 2, 2 -> 3, 3 -> 1, 2 -> 4, 4 -> 1, 1 <-> 5] and get six goals like |- p1 -> p2 and |- p1 <-> p5

[Johan Commelin]

@Reid Barton Hmmm... but then it feels like you'll need a separate mode, like conv and calc.

[Mario Carneiro]

ooh, should it be zero-based indexing?

[Johan Commelin]

In principal that is fine, but in practice we see that conv is limited by the fact that not all tactics that we'dd like to be there actually work.

[Johan Commelin]

I guess 0-based is easier to implement. But I don't know if it is user friendly.

[Mario Carneiro]

1 based is probably more user friendly, but I'm sure it will surprise someone either way

[Johan Commelin]

@Mario Carneiro Do you think Reid's idea can be implemented in usual tactic mode?

[Reid Barton]

maybe rather than a plain list in tfae we should use an association list indexed by
inductive roman_number | i | ii | iii | iv | ...

[Mario Carneiro]

and how long does that ... go? :P

[Johan Commelin]

at least till xiii

[Mario Carneiro]

anyway it's not an actual type, it's just an input format

[Mario Carneiro]

1 -> 2 isn't well typed

[Reid Barton]

What I really mean though is if you actually had 13 things to prove equivalent, you wouldn't really want to have to count them whether you use 0-based or 1-based indexing

[Mario Carneiro]

neither is i -> ii

[Mario Carneiro]

I don't see an alternative

[Mario Carneiro]

lean can try to give you help in filling out the tactic arguments, but that's it

[Johan Commelin]

@Reid Barton Do you have an idea for an "interleaving UI"?

[Johan Commelin]

syntax, I mean

[Johan Commelin]

What would you like to write?

[Mario Carneiro]

it sounds like what case does, but in that case you already know what the goals are

[Reid Barton]

something like case in terms of syntax, yeah

[Johan Commelin]

have : i -> ii := bla

[Mario Carneiro]

tfae could take an itactic argument, I'm not sure if the parsing will work but then you could have one huge tactic with subblocks like:

tfae:
1 -> 2 {
  ...
}
2 -> 1 {
  ...
},

[Johan Commelin]

And then, somehow Lean should keep track of them. And once you think you are done, you type tfae_done, and it checks that your graph is SC.

[Mario Carneiro]

in my example it's just one tactic invocation (note lack of comma)

[Johan Commelin]

I see. And inside the { ... } you would be in regular tactic mode?

[Mario Carneiro]

yes

[Johan Commelin]

Then I think that syntax is really cool!

[Mario Carneiro]

I don't know if I can make it work though

[Mario Carneiro]

itactic isn't a parser

[Johan Commelin]

I know that I can't

[Johan Commelin]

I think I would call the tactic tfae_cases

[Mario Carneiro]

I would stick to my original proposal though, these syntaxes are crazy

[Mario Carneiro]

you can put the numbers in comments if you forgot which is which

[Johan Commelin]

Ok, too bad.

[Johan Commelin]

But, if you think it is really hard to do, then I won't even try thinking about it (-;

[Mario Carneiro]

also you could have tfae? which would just print out a numbered list of the elements of the tfae for referral

[Johan Commelin]

It should be a hole command (-;

[Johan Commelin]

And fill out those comments!

[Mario Carneiro]

I want more "implicit" hole commands (without the {!!} markers), but alas

[Johan Commelin]

Mario, could we have have : tfae_case i ii := ...

[Johan Commelin]

and then a finishing tactic tfae_done

[Reid Barton]

Oh, have is a better analogy. I would certainly be happy with have_tfae 1 -> 3, blah, have_tfae ..., ..., tfae_finish

[Mario Carneiro]

sorry, that's not well typed. The best you can do is have : p1 -> p2 and have tfae_done figure it out

[Johan Commelin]

But it's just notation, like before...

[Johan Commelin]

Ok, my example won't work.

[Johan Commelin]

But Reid's could, not?

[Reid Barton]

It would need to refer to the goal

[Reid Barton]

Yours I mean

[Mario Carneiro]

Actually have_tfae 1 -> 3 might make sense: if the goal is tfae [p1, ..., p5] then it is just the same as have : p1 -> p3

[Johan Commelin]

Exactly. (And can we make it tfae_have?)

[Reid Barton]

It should also support <-> btw

[Johan Commelin]

So the tfae_have should generate a new goal, and record an edge in some graph. And then tfae_finish checks that the graph is SC.

[Mario Carneiro]

naturally

[Johan Commelin]

I really like where this is going!

[Mario Carneiro]

tfae_have doesn't need to do anything

[Reid Barton]

tfae_finish could almost just be solve_by_elim it seems

[Johan Commelin]

A smart tfae_finish could suggest a list of edges that still needs to be done...

[Mario Carneiro]

tfae_finish has to apply tfae_of_cycle, reduce the subproofs to implications of the given stuff, and then use the existing implications

[Mario Carneiro]

and produce any unproven parts as subgoals

[Mario Carneiro]

that way you can use tfae either forwards or backwards

[Johan Commelin]

What would those unproven parts look like?

[Johan Commelin]

Just unproven edges in the default cycle?

[Mario Carneiro]

yes

[Johan Commelin]

Ok, so by default tfae_finish generates n goals.

[Mario Carneiro]

(I would just call this one tfae btw)

[Johan Commelin]

If you want to use it both forwards and backward, that makes sense.

[Johan Commelin]

Semantically I don't like tfae, but short names are useful.

[Mario Carneiro]

tfae can still take a list of edges, and it would just add to this the list of edges that have already been have'd

[Johan Commelin]

Ok, once this tactic is there, we need to make sure obviously in fact tackles the first nine cases of the Hensel's lemma TFAE proof.

[Reid Barton]

tpwe = the preceding were equivalent for the finisher

[Cyril Cohen]

you can put the numbers in comments if you forgot which is which

That's what I do

[Keeley Hoek]

@Mario Carneiro is there a version of chain which lets me apply a function to each pair?

[Scott Morrison]

What do you mean, @Keeley Hoek?

[Keeley Hoek]

id like to apply an α → α → β function to pairs of adjacent elements of a list α, and get a list β. It feels a bit like chain but not just for Props

[Johan Commelin]

@Mario Carneiro Are you working on this tactic? Or do you think this could be a good exercise for me trying to learn how to write tactics?

[Mario Carneiro]

I'm not working on it right now. If you would like to try your hand at it, go ahead

[Mario Carneiro]

@Keeley Hoek I would suggest defining an element of α × β using list.foldl

[Johan Commelin]

@Reid Barton @Simon Hudon and me have worked on this a bit. There is now a PR: https://github.com/leanprover/mathlib/pull/373

[Johan Commelin]

@Johannes Hölzl @Mario Carneiro Is there anything blocking this PR? I've been hitting a couple of "the following are equivalent" lemmas recently, and I wouldn't mind using this machinery.

[Johannes Hölzl]

Looks good for me. I'm fine with merging it.

[Johannes Hölzl]

I don't know if Mario still has some concerns?

[Mario Carneiro]

no, I have just been busy with school. Go ahead and merge it if you have looked it over.

[Johannes Hölzl]

okay I merged it