John Hughes (Sep 22 2025 at 17:02): John Hughes (Sep 22 2025 at 17:02):I'm trying to show that each item of some datatype lies in 3 of the subsets in a list of subsets of that datatype:
theory test
imports Main
begin
datatype pointD = Hd | Ad | Bd | Cd| Dd| Ed| Fd| Pd | Qd |Rd
definition LinesD::"pointD set set" where
"LinesD ={{Ad,Bd, Pd}, {Bd, Cd,Rd}, {Cd, Ad, Qd}, {Dd, Ed, Pd}, {Ed, Fd, Rd}, {Fd, Dd, Qd},
{Hd, Ad, Dd}, {Hd, Bd, Ed}, {Hd, Cd, Fd}, {Pd, Qd, Rd}}"
lemma desargues_three_lines: (* every pt lies on 3 lines *)
fixes X::"pointD"
assumes "X = Ad" (* an extreme case...can we prove this even with X known *)
shows "∃ l m n . distinct[l, m, n] ∧
X ∈ l ∧ X ∈ m ∧ X ∈ n ∧
l ∈ LinesD ∧ m ∈ LinesD ∧ n ∈ LinesD"
using LinesD_def pointD.exhaust by sledgehammer
end
This claim seems completely evident to me, but sledgehammer is getting nowhere. As you can see, I've tried to reduce the problem by a factor of ten and simple show that the point Ad lies in three of the "Lines"; even this seems to be too much. (The lines are right there: {Ad,Bd, Pd}, {Cd, Ad, Qd}, {Hd, Ad, Dd}, but apparently I don't have the right magic to make it easy for Isabelle to see this.)
Of course, I'd like to show the 10-times-harder claim that leaves out that assumption.
Can someone nudge me in the right direction? (BTW, I'm trying to do this with Isar rather than apply-style proofs, although I'm not sure how I'd do it even if I were using apply.)
Mathias Fleury (Sep 22 2025 at 17:46):Ahh my favorite kind of proofs: the useless proofs where you fight the simplifier and auto to do the right thing. I managed to get it a 40s (!) one-liner:
lemma desargues_three_lines: (* every pt lies on 3 lines *)
fixes X::"pointD"
shows "∃ l m n . distinct[l, m, n] ∧
X ∈ l ∧ X ∈ m ∧ X ∈ n ∧
l ∈ LinesD ∧ m ∈ LinesD ∧ n ∈ LinesD"
proof -
have [simp]:
‹{Hd, Cd, Fd} ≠ {Hd, Bd, Ed}›
‹{Hd, Cd, Fd} ≠ {Hd, Ad, Dd}›
‹{Hd, Bd, Ed} ≠ {Hd, Ad, Dd}›
‹{Hd, Ad, Dd} ≠ {Cd, Ad, Qd}›
‹{Hd, Ad, Dd} ≠ {Ad, Bd, Pd}›
‹{Cd, Ad, Qd} ≠ {Ad, Bd, Pd}›
‹ {Hd, Bd, Ed} ≠ {Bd, Cd, Rd}›
‹{Hd, Bd, Ed} ≠ {Ad, Bd, Pd}›
‹{Bd, Cd, Rd} ≠ {Ad, Bd, Pd}›
‹{Hd, Cd, Fd} ≠ {Cd, Ad, Qd}›
‹{Hd, Cd, Fd} ≠ {Bd, Cd, Rd}›
‹{Cd, Ad, Qd} ≠ {Bd, Cd, Rd}›
‹{Hd, Ad, Dd} ≠ {Fd, Dd, Qd}›
‹{Hd, Ad, Dd} ≠ {Dd, Ed, Pd}›
‹{Fd, Dd, Qd} ≠ {Dd, Ed, Pd}›
‹{Hd, Bd, Ed} ≠ {Ed, Fd, Rd}›
‹{Hd, Bd, Ed} ≠ {Dd, Ed, Pd}›
‹{Ed, Fd, Rd} ≠ {Dd, Ed, Pd}›
‹{Hd, Cd, Fd} ≠ {Fd, Dd, Qd}›
‹{Hd, Cd, Fd} ≠ {Ed, Fd, Rd}›
‹{Fd, Dd, Qd} ≠ {Ed, Fd, Rd}›
‹{Pd, Qd, Rd} ≠ {Dd, Ed, Pd}›
‹{Pd, Qd, Rd} ≠ {Ad, Bd, Pd}›
‹{Dd, Ed, Pd} ≠ {Ad, Bd, Pd}›
‹{Pd, Qd, Rd} ≠ {Fd, Dd, Qd}›
‹{Pd, Qd, Rd} ≠ {Cd, Ad, Qd}›
‹{Fd, Dd, Qd} ≠ {Cd, Ad, Qd}›
‹{Pd, Qd, Rd} ≠ {Ed, Fd, Rd}›
‹{Pd, Qd, Rd} ≠ {Bd, Cd, Rd}›
‹{Ed, Fd, Rd} ≠ {Bd, Cd, Rd}›
by auto
show ?thesis
by (cases X)
(simp only: insert_iff empty_iff LinesD_def conj_disj_distribL conj_disj_distribR ex_disj_distrib
simp_thms(39); simp; fail)+
qed
If you are not afraid of using normalization oracles:
lemma desargues_three_lines: (* every pt lies on 3 lines *)
fixes X :: pointD
shows "∃(l, m, n) ∈ LinesD × LinesD × LinesD. distinct [l, m, n] ∧ X ∈ l ∧ X ∈ m ∧ X ∈ n"
apply (cases X; hypsubst)
apply normalization+ (*or eval*)
done
Mathias Fleury said:
Ahh my favorite kind of proofs: the useless proofs where you fight the simplifier and auto to do the right thing. I managed to get it a 40s (!) one-liner:
...
Now I'm thankful that the Desargues configuration is the most complex I need to discuss. :) I'm astounded that the first fact -- that all those triples are distinct -- needs to be supplied to simp. The by (cases X) ... proof uses a structure that I've never seen . In my limited worldview, by is followed by a prover-name (like metis or simp or auto and possibly some arguments. I guess that the (simp only:...) is an instance of that. The + at the end presumably means "do it over and over" --- that's nice. But the (by cases) is something I'd expect to see only in the form
show ?thesis
proof (cases X)
show ?thesis by (simp only: ...)
I guess I'm headed back to the reference manual to learn a few more constructs. Thanks for both (1) pushing me towards learning a few new things and (2) confirming that this is really just as annoying as it appeared to be!
John Hughes (Sep 22 2025 at 19:48):Kevin Kappelmann said:
lemma desargues_three_lines: (* every pt lies on 3 lines *) fixes X :: pointD shows "∃(l, m, n) ∈ LinesD × LinesD × LinesD. distinct [l, m, n] ∧ X ∈ l ∧ X ∈ m ∧ X ∈ n" apply (cases X; hypsubst) apply normalization+ (*or eval*) done
I've managed to rewrite this in Isar without the slightest understanding of what I've done, by patching together your answer with Mathias's:
proof -
show ?thesis
by (cases X; hypsubst; normalization+)
end
Now I just have to go decode whatever it is I've managed to do! Thank you!
Last updated: Oct 12 2025 at 20:20 UTC