## Stream: general

### Topic: TFAE

#### Reid Barton (Sep 07 2018 at 19:52):

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 (Sep 07 2018 at 20:01):

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 (Sep 08 2018 at 03:47):

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

#### Mario Carneiro (Sep 08 2018 at 03:51):

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 (Sep 08 2018 at 03:52):

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 (Sep 08 2018 at 03:53):

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

#### Mario Carneiro (Sep 08 2018 at 03:54):

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 (Sep 08 2018 at 04:26):

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 (Sep 08 2018 at 04:30):

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

yep ok sure

#### Reid Barton (Sep 08 2018 at 08:21):

(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 (Sep 08 2018 at 09:32):

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

#### Reid Barton (Sep 08 2018 at 09:45):

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 (Sep 08 2018 at 09:58):

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 (Sep 08 2018 at 23:54):

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 (Sep 08 2018 at 23:56):

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 (Sep 09 2018 at 00:01):

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

#### Mario Carneiro (Sep 09 2018 at 00:02):

Also, that's a quadratic number of generated lemmas

#### Simon Hudon (Sep 09 2018 at 00:06):

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

I'm fairly sure that you can.

#### Simon Hudon (Sep 09 2018 at 00:08):

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 (Sep 09 2018 at 00:16):

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

#### Mario Carneiro (Sep 09 2018 at 00:18):

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 (Sep 09 2018 at 00:19):

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

#### Mario Carneiro (Sep 09 2018 at 00:19):

then again, simp already does that

#### Kenny Lau (Sep 09 2018 at 00:21):

wow that's so magical

#### Mario Carneiro (Sep 09 2018 at 00:37):

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 (Sep 11 2018 at 16:59):

@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 (Sep 11 2018 at 17:55):

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

#### Cyril Cohen (Sep 12 2018 at 11:23):

@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 (Sep 12 2018 at 11:30):

That looks like a really nice way to attack this.

#### Johan Commelin (Sep 12 2018 at 11:32):

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 (Sep 12 2018 at 11:33):

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)

Right.

#### Johan Commelin (Sep 12 2018 at 11:34):

But it would allow for more convenience.

Yes

#### Johan Commelin (Sep 12 2018 at 11:35):

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 (Sep 12 2018 at 11:35):

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

#### Johan Commelin (Sep 12 2018 at 11:37):

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

#### Cyril Cohen (Sep 12 2018 at 11:37):

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 (Sep 12 2018 at 11:38):

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

#### Johan Commelin (Sep 12 2018 at 11:38):

But do you have henselian local rings?

Just kidding...

#### Johan Commelin (Sep 12 2018 at 11:39):

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

#### Johan Commelin (Sep 12 2018 at 11:39):

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

it is just a dfs

#### Johan Commelin (Sep 12 2018 at 11:40):

/me walks over to his copy of TAOCP

#### Johan Commelin (Sep 12 2018 at 11:40):

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

#### Johan Commelin (Sep 12 2018 at 11:41):

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

#### Johan Commelin (Sep 12 2018 at 11:42):

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

#### Johan Commelin (Sep 12 2018 at 11:43):

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

#### Cyril Cohen (Sep 12 2018 at 11:47):

@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 (Sep 12 2018 at 11:50):

Ok, understood :thumbs_up:

#### Patrick Massot (Sep 12 2018 at 11:55):

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 (Sep 12 2018 at 11:57):

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

ok, nice

#### Patrick Massot (Sep 12 2018 at 12:11):

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 (Sep 12 2018 at 12:13):

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 (Sep 12 2018 at 12:16):

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

#### Reid Barton (Sep 12 2018 at 12:24):

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 (Sep 12 2018 at 12:42):

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 (Sep 12 2018 at 12:42):

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 (Sep 12 2018 at 12:45):

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 (Sep 12 2018 at 12:45):

which lets you guarantee that the list is nonempty

#### Johan Commelin (Sep 12 2018 at 12:48):

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 (Sep 12 2018 at 12:50):

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

#### Reid Barton (Sep 12 2018 at 12:51):

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 (Sep 12 2018 at 12:55):

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 (Sep 12 2018 at 12:56):

True, something like that is necessary.

#### Johan Commelin (Sep 12 2018 at 13:04):

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

#### Johan Commelin (Sep 12 2018 at 13:05):

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 (Sep 12 2018 at 13:05):

Do you case on i < j or something similar?

#### Cyril Cohen (Sep 12 2018 at 13:09):

@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 (Sep 12 2018 at 13:10):

Hmm, I see. That seems smart.

#### Johan Commelin (Sep 12 2018 at 13:11):

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

#### Kenny Lau (Sep 12 2018 at 13:12):

is it even in mathlib?

#### Kenny Lau (Sep 12 2018 at 13:12):

I'd just use induction to prove it

Dunno.

#### Johan Commelin (Sep 12 2018 at 13:22):

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 (Sep 12 2018 at 13:22):

It still needs a name and golfing (-;

#### Johan Commelin (Sep 12 2018 at 14:37):

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

#### Johan Commelin (Sep 12 2018 at 14:46):

@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 (Sep 12 2018 at 15:07):

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

constants a b : Prop

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


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

#### Keeley Hoek (Sep 12 2018 at 15:09):

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

#### Keeley Hoek (Sep 12 2018 at 15:22):

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 (Sep 12 2018 at 16:53):

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

#### Mario Carneiro (Sep 12 2018 at 17:14):

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

#### Keeley Hoek (Sep 12 2018 at 17:21):

that list.chain syntax is sick Mario

#### Mario Carneiro (Sep 12 2018 at 17:46):

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 (Sep 12 2018 at 17:49):

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 (Sep 12 2018 at 17:53):

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

#### Mario Carneiro (Sep 12 2018 at 17:54):

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

#### Mario Carneiro (Sep 12 2018 at 17:55):

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

#### Johan Commelin (Sep 12 2018 at 17:56):

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

#### Johan Commelin (Sep 12 2018 at 17:56):

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

#### Johan Commelin (Sep 12 2018 at 17:57):

I think we should put everything into a tfae namespace.

#### Mario Carneiro (Sep 12 2018 at 17:58):

I would just put it all in list.basic

#### Mario Carneiro (Sep 12 2018 at 17:58):

and in the list namespace, as you can see

#### Johan Commelin (Sep 12 2018 at 17:58):

Ok, fine with me.

#### Johan Commelin (Sep 12 2018 at 17:58):

Do you want to capitalise TFAE?

#### Mario Carneiro (Sep 12 2018 at 17:59):

dunno, seemed nicer that way

#### Mario Carneiro (Sep 12 2018 at 17:59):

tfae could be misread?

#### Johan Commelin (Sep 12 2018 at 17:59):

Maybe. TFAE feels like shouting.

#### Johan Commelin (Sep 12 2018 at 17:59):

I wouldn't mind having tfae.

#### Mario Carneiro (Sep 12 2018 at 17:59):

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

#### Johan Commelin (Sep 12 2018 at 18:00):

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

#### Mario Carneiro (Sep 12 2018 at 18:01):

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

#### Mario Carneiro (Sep 12 2018 at 18:01):

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

#### Johan Commelin (Sep 12 2018 at 18:02):

Right, I also came to that conclusion

#### Johan Commelin (Sep 12 2018 at 18:02):

It is even easier to read.

#### Mario Carneiro (Sep 12 2018 at 18:02):

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

#### Johan Commelin (Sep 12 2018 at 18:03):

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

#### Johan Commelin (Sep 12 2018 at 18:03):

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 (Sep 12 2018 at 18:09):

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

Why not?

#### Mario Carneiro (Sep 12 2018 at 18:10):

because the number of goals is very nonuniform

#### Mario Carneiro (Sep 12 2018 at 18:10):

the types are too complicated to get much help from lean

#### Mario Carneiro (Sep 12 2018 at 18:11):

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

#### Mario Carneiro (Sep 12 2018 at 18:12):

in lean we would do it with a tactic

#### Johan Commelin (Sep 12 2018 at 18:15):

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 (Sep 12 2018 at 18:15):

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

#### Mario Carneiro (Sep 12 2018 at 18:16):

You would have to supply proofs manually which is not nice

#### Johan Commelin (Sep 12 2018 at 18:16):

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

#### Johan Commelin (Sep 12 2018 at 18:17):

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

#### Patrick Massot (Sep 12 2018 at 18:17):

this would not be interactive because of the proofs parameter

#### Johan Commelin (Sep 12 2018 at 18:17):

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

#### Mario Carneiro (Sep 12 2018 at 18:17):

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 (Sep 12 2018 at 18:17):

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

What is SC?

#### Mario Carneiro (Sep 12 2018 at 18:18):

strongly connected

I see.

#### Mario Carneiro (Sep 12 2018 at 18:19):

if true, the generalization is always redundant

#### Mario Carneiro (Sep 12 2018 at 18:20):

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 (Sep 12 2018 at 18:20):

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

of course

#### Johan Commelin (Sep 12 2018 at 18:21):

Did I misunderstand your conjecture?

#### Mario Carneiro (Sep 12 2018 at 18:21):

so I guess we need a theorem about permuting the graph

#### Mario Carneiro (Sep 12 2018 at 18:21):

no, that's a counterexample

#### Johan Commelin (Sep 12 2018 at 18:22):

I'dd just do a meta dfs

#### Mario Carneiro (Sep 12 2018 at 18:22):

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

That is trivial

is it?

Hmm, maybe not.

#### Johan Commelin (Sep 12 2018 at 18:24):

But, why do you not want to reuse edges?

#### Mario Carneiro (Sep 12 2018 at 18:25):

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

#### Mario Carneiro (Sep 12 2018 at 18:25):

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

#### Mario Carneiro (Sep 12 2018 at 18:26):

so it doesn't need to be stored and reused

#### Johan Commelin (Sep 12 2018 at 18:26):

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

foiled again

#### Johan Commelin (Sep 12 2018 at 18:29):

Hmm, you don't even need vertex 5.

#### Mario Carneiro (Sep 12 2018 at 18:29):

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

#### Johan Commelin (Sep 12 2018 at 18:30):

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

yes

#### Reid Barton (Sep 12 2018 at 18:31):

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

#### Patrick Massot (Sep 12 2018 at 18:31):

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 (Sep 12 2018 at 18:32):

No, you provide a list of edges.

#### Johan Commelin (Sep 12 2018 at 18:32):

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

#### Patrick Massot (Sep 12 2018 at 18:32):

ok, I prefer that

#### Reid Barton (Sep 12 2018 at 18:32):

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

#### Mario Carneiro (Sep 12 2018 at 18:33):

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 (Sep 12 2018 at 18:33):

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

#### Mario Carneiro (Sep 12 2018 at 18:34):

ooh, should it be zero-based indexing?

#### Johan Commelin (Sep 12 2018 at 18:34):

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 (Sep 12 2018 at 18:35):

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

#### Mario Carneiro (Sep 12 2018 at 18:35):

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

#### Johan Commelin (Sep 12 2018 at 18:36):

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

#### Reid Barton (Sep 12 2018 at 18:36):

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 (Sep 12 2018 at 18:36):

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

#### Johan Commelin (Sep 12 2018 at 18:37):

at least till xiii

#### Mario Carneiro (Sep 12 2018 at 18:37):

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

#### Mario Carneiro (Sep 12 2018 at 18:37):

1 -> 2 isn't well typed

#### Reid Barton (Sep 12 2018 at 18:37):

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 (Sep 12 2018 at 18:37):

neither is i -> ii

#### Mario Carneiro (Sep 12 2018 at 18:38):

I don't see an alternative

#### Mario Carneiro (Sep 12 2018 at 18:38):

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

#### Johan Commelin (Sep 12 2018 at 18:39):

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

syntax, I mean

#### Johan Commelin (Sep 12 2018 at 18:39):

What would you like to write?

#### Mario Carneiro (Sep 12 2018 at 18:39):

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

#### Reid Barton (Sep 12 2018 at 18:40):

something like case in terms of syntax, yeah

#### Johan Commelin (Sep 12 2018 at 18:40):

have : i -> ii := bla

#### Mario Carneiro (Sep 12 2018 at 18:41):

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 (Sep 12 2018 at 18:41):

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 (Sep 12 2018 at 18:42):

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

#### Johan Commelin (Sep 12 2018 at 18:42):

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

yes

#### Johan Commelin (Sep 12 2018 at 18:42):

Then I think that syntax is really cool!

#### Mario Carneiro (Sep 12 2018 at 18:43):

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

#### Mario Carneiro (Sep 12 2018 at 18:43):

itactic isn't a parser

#### Johan Commelin (Sep 12 2018 at 18:43):

I know that I can't

#### Johan Commelin (Sep 12 2018 at 18:43):

I think I would call the tactic tfae_cases

#### Mario Carneiro (Sep 12 2018 at 18:45):

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

#### Mario Carneiro (Sep 12 2018 at 18:46):

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

#### Johan Commelin (Sep 12 2018 at 18:47):

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

#### Mario Carneiro (Sep 12 2018 at 18:47):

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

#### Johan Commelin (Sep 12 2018 at 18:48):

It should be a hole command (-;

#### Johan Commelin (Sep 12 2018 at 18:48):

And fill out those comments!

#### Mario Carneiro (Sep 12 2018 at 18:48):

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

#### Johan Commelin (Sep 12 2018 at 18:50):

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

#### Johan Commelin (Sep 12 2018 at 18:50):

and then a finishing tactic tfae_done

#### Reid Barton (Sep 12 2018 at 18:50):

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

#### Mario Carneiro (Sep 12 2018 at 18:51):

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

#### Johan Commelin (Sep 12 2018 at 18:51):

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

#### Johan Commelin (Sep 12 2018 at 18:52):

Ok, my example won't work.

#### Johan Commelin (Sep 12 2018 at 18:52):

But Reid's could, not?

#### Reid Barton (Sep 12 2018 at 18:52):

It would need to refer to the goal

Yours I mean

#### Mario Carneiro (Sep 12 2018 at 18:52):

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 (Sep 12 2018 at 18:52):

Exactly. (And can we make it tfae_have?)

#### Reid Barton (Sep 12 2018 at 18:53):

It should also support <-> btw

#### Johan Commelin (Sep 12 2018 at 18:53):

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.

naturally

#### Johan Commelin (Sep 12 2018 at 18:54):

I really like where this is going!

#### Mario Carneiro (Sep 12 2018 at 18:54):

tfae_have doesn't need to do anything

#### Reid Barton (Sep 12 2018 at 18:54):

tfae_finish could almost just be solve_by_elim it seems

#### Johan Commelin (Sep 12 2018 at 18:55):

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

#### Mario Carneiro (Sep 12 2018 at 18:55):

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 (Sep 12 2018 at 18:56):

and produce any unproven parts as subgoals

#### Mario Carneiro (Sep 12 2018 at 18:56):

that way you can use tfae either forwards or backwards

#### Johan Commelin (Sep 12 2018 at 18:57):

What would those unproven parts look like?

#### Johan Commelin (Sep 12 2018 at 18:57):

Just unproven edges in the default cycle?

yes

#### Johan Commelin (Sep 12 2018 at 18:57):

Ok, so by default tfae_finish generates n goals.

#### Mario Carneiro (Sep 12 2018 at 18:58):

(I would just call this one tfae btw)

#### Johan Commelin (Sep 12 2018 at 18:58):

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

#### Johan Commelin (Sep 12 2018 at 18:59):

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

#### Mario Carneiro (Sep 12 2018 at 18:59):

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 (Sep 12 2018 at 19:04):

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 (Sep 12 2018 at 19:09):

tpwe = the preceding were equivalent for the finisher

#### Cyril Cohen (Sep 13 2018 at 07:00):

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

That's what I do

#### Keeley Hoek (Sep 13 2018 at 09:33):

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

#### Scott Morrison (Sep 13 2018 at 09:36):

What do you mean, @Keeley Hoek?

#### Keeley Hoek (Sep 13 2018 at 09:44):

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 (Sep 13 2018 at 17:07):

@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 (Sep 13 2018 at 17:08):

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

#### Mario Carneiro (Sep 13 2018 at 17:08):

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

#### Johan Commelin (Sep 26 2018 at 15:52):

@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 (Oct 04 2018 at 08:33):

@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 (Oct 04 2018 at 08:37):

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

#### Johannes Hölzl (Oct 04 2018 at 08:37):

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

#### Mario Carneiro (Oct 04 2018 at 13:02):

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

#### Johannes Hölzl (Oct 04 2018 at 13:08):

okay I merged it

Last updated: Dec 20 2023 at 11:08 UTC