Proof by "the following are equivalent" #373
Conversation
equivalent propositions which can be proved equivalent by cyclical implications
docs/tactics.md
Outdated
| expression of the form `i arrow j`, where `i` and `j` are two positive | ||
| natural numbers, and `arrow` is an arrow such as `→`, `->`, `←`, `<-`, | ||
| `↔`, or `<->`. The tactic `tfae_have : i arrow j` sets up a subgoal in | ||
| which the user |
There was a problem hiding this comment.
What's the end of the sentence?
docs/tactics.md
Outdated
| `↔`, or `<->`. The tactic `tfae_have : i arrow j` sets up a subgoal in | ||
| which the user | ||
|
|
||
| The remaining tactics, `tfae_finish`, is a finishing tactic. It |
|
|
||
| Data structures and algorithms for finding the sets of equivalent | ||
| proposition in a set of implications. | ||
| -/ |
There was a problem hiding this comment.
What does scc stands for?
There was a problem hiding this comment.
strongly connected components in graph theory. I can add that to the header.
tactic/scc.lean
Outdated
| do `(%%p ↔ %%q) ← target >>= whnf, | ||
| cl.prove_eqv p q >>= exact | ||
|
|
||
| meta def interactive.check_eqv : tactic unit := |
There was a problem hiding this comment.
This is an interactive tactic but doesn't seem documented. Same remark for other tactics below.
data/list/basic.lean
Outdated
| @@ -3849,6 +3849,54 @@ def map_last {α} (f : α → α) : list α → list α | |||
| | [x] := [f x] | |||
| | (x :: xs) := x :: map_last xs | |||
|
|
|||
| /- tfae: The Following (propositions) Are Equivalent -/ | |||
There was a problem hiding this comment.
this comment should be a doc comment on tfae
tactic/scc.lean
Outdated
| p₂ ← mk_app ``iff.symm [p₀], | ||
| p ← mk_app ``iff.trans [p₂,p], | ||
| p ← mk_app ``iff.trans [p,p₁], | ||
| m ← read_ref cl, |
tactic/scc.lean
Outdated
| do (r,p₀) ← root cl e₀, | ||
| (r',p₁) ← root cl e₁, | ||
| b ← try_core $ is_def_eq r r', | ||
| pure b.is_some |
| rewrite_target tfae_cons, split, | ||
| prove_eqv_target cl }, | ||
| applyc ``tfae_singleton, | ||
| pure ()) |
There was a problem hiding this comment.
It seems like scc likes to prove everything equivalent to a "root" vertex. So why don't you use a tfae constructor of that form?
There was a problem hiding this comment.
What form do you mean?
There was a problem hiding this comment.
Something like this:
theorem tfae_iff_forall : tfae (a :: l) ↔ ∀ b ∈ l, a ↔ b
Not sure if you always pick the root to be the first vertex or you prefer some other vertex, in which case this can be modified.
There was a problem hiding this comment.
I see what you mean. No, there's no determination of which one is being used. There's also no guarantee that the root is part of the list, in case you prove implications with other propositions and that they contribute to the cycles.
There was a problem hiding this comment.
In that case, you could use this:
theorem tfae_of_forall (a : Prop) (h : ∀ b ∈ l, a ↔ b) : tfae l
There was a problem hiding this comment.
That's true, that would work. Are you preferring this approach because it will produce smaller proof terms or do you also think it will be faster?
There was a problem hiding this comment.
I just made the change and pushed it.
|
looks good for me |
tactic for decomposing a proof into a set of equivalent propositions which can be proved equivalent by cyclical implications
With @jcommelin @rwbarton and @digama0.
TO CONTRIBUTORS:
Make sure you have:
For reviewers: code review check list