Extremely trivial:
The last line doesn't work, any idea how to fix? Is there a way to say: let h be the proof of the antecedent; obtain a,b from h; now use a,b to prove the consequent, the way one can do in Lean?
$\begingroup$
$\endgroup$
Add a comment
|
2 Answers
$\begingroup$
$\endgroup$
3
You probably need to add some type annotations. Even in Isabelle/ZF where type annotations are very rarely needed in this case one has to write
lemma "(∃y::i. ∃x::i. x≠y) ⟶ (∃y::i. ∃x::i. x≠y)" by auto
A proof that obtains x,y from the antecedent would look similar to this:
lemma "(∃y::i. ∃x::i. x≠y) ⟶ (∃y::i. ∃x::i. x≠y)"
proof
assume "∃y::i. ∃x::i. x≠y"
then obtain y::i where "∃x::i. x≠y" by auto
then obtain x::i where "x≠y" by auto
thus "∃y::i. ∃x::i. x≠y" by auto
qed
-
$\begingroup$ Thanks, but now I get
undefined type name i. Usingnatinstead ofiworked though. $\endgroup$ Commented Jun 2 at 22:05 -
1$\begingroup$ My example is in Isabelle/ZF. You probably work with Isabelle/HOL. $\endgroup$ Commented Jun 3 at 6:09
-
$\begingroup$ @BjørnKjos-Hanssen any type variable will do in HOL, as in
lemma "(∃y::'a. ∃x. x≠y) ⟶ (∃y::'a. ∃x. x≠y)" by auto(as far as it appears at least once in both antecedent and consecuent). $\endgroup$ Commented Jun 7 at 14:19
$\begingroup$
$\endgroup$
As I wrote in the comment above, it suffices to add one (and the same) type variable.
But I believe the result is not true in full generality, since there are types with one element. Note that unit is not necessarilly such type! Because every type in HOL has the undefined element. In any case the following theory is a bit misleading:
theory Scratch
imports Main
begin
typedef reallyunit = "{undefined::nat}"
by auto
lemma "(∃y::'a. ∃x. x≠y) ⟶ (∃y::'a. ∃x. x≠y)"
by auto (* succeeds *)
lemma "(∃y. ∃x::unit. x≠y) ⟶ (∃y::reallyunit. ∃x. x≠y)"
by auto (* succeeds *)
lemma "(∃y. ∃x::nat. x≠y) ⟶ (∃y::reallyunit. ∃x. x≠y)"
try0 (* fails *)
oops
end
answered Jun 7 at 14:33