3 ms·

Funny I came to complain that the final version of this exact proof is not human readable any more: Theorem sqrt2_not_rational : forall p q : nat, q <> 0 -> p

by singularity2001 8y ago

Funny I came to complain that the final version of this exact proof is not human readable any more: Theorem sqrt2_not_rational : forall p q : nat, q <> 0 -> p x p = 2 x (q x q) -> False. intros p q; generalize p; clear p; elim q using (well_founded_ind lt_wf). clear q; intros q Hrec p Hneq; generalize (neq_O_lt _ (sym_not_equal Hneq)); intros Hlt_O_q Heq. apply (Hrec (3 x q - 2 x p) (comparison4 _ _ Hlt_O_q Heq) (3 x p - 4 x q)). apply sym_not_equal; apply lt_neq; apply plus_lt_reg_l with (2 x p); rewrite <- plus_n_O; rewrite <- le_plus_minus; auto with x. apply new_equality; auto. Qed. This doesn't have to be. Maybe the author assumed that the audience knows the proof by heart. I don't, I know a proof but none including (3 * q - 2 * p). So longer names and comments please, ideally in a way understandable both by humans and machines. Or the goal was to 'get the proof done' with maximal brevity. Then please don't include it in the 'show off' page. In a future version of coq 'sqrt2_not_rational' might be spelled out "Theorem: sqare_root(2) not rational" PS: stupid HN removing unicode signs

ekidd 8y ago
> the final version of this exact proof is not human readable any more: In general, Coq proofs are meant to be read using tools, not as plain text. You start out with the theorem you want to prove, and you apply a rule to it. Then Coq shows two new things to prove. You apply a rule to each of these, and so on. Without seeing the list of active "proof goals" at each step, there's no way to guess what "apply sym_not_equal" means. But if you step through the proof line-by-line in the editor, then you can examine how each step updates your "proof goals". (I have an old blog post that shows what this looks like: http://www.randomhacks.net/2015/07/19/proving-sorted-lists-correct-using-coq-proof-assistent/ http://www.randomhacks.net/2015/07/19/proving-sorted-lists-c...) I admit, it can still be pretty arcane. But with the right tools and a bit of experience, it does get a lot easier. The real head-scratcher are advanced "proof tactics" like "auto", which automatically apply a long lists of possible transformations until they find an answer: Theorem basic_conj' : forall (A B : Prop), A -> B -> A /\ B. Proof. auto. Qed. This is the Coq version of "the proof is left as a exercise for the computer." It's pretty cool technology if you like math, well worth some time to puzzle it out. But expect to have to read some tutorials and think about them.
gus_massa 8y ago
> I don't, I know a proof but none including (3 . q - 2 . p). It's weird. I'm still looking at it. It would be nice to have an explanation here by someone that is a Coq specialist. Anyway, in a google search found this other proof that uses that > The last digit of the square of any positive integer written in base 3 can not be 2. [near a reference to Robert Gauntt] http://www.mathpath.org/proof/sqrt2.irrat.htm http://www.mathpath.org/proof/sqrt2.irrat.htm I'm not sure that it is related, but the 3q-2p and 3p-4q look like something that can be related to base 3. It looks like the base 3 proof doesn't use the Fundamental Theorem of Arithmetic, that is a very powerful result and I'm not sure if they have already a formal demonstration of that in Coq.

ekidd 8y ago

> the final version of this exact proof is not human readable any more: In general, Coq proofs are meant to be read using tools, not as plain text. You start out with the theorem you want to prove, and you apply a rule to it. Then Coq shows two new things to prove. You apply a rule to each of these, and so on. Without seeing the list of active "proof goals" at each step, there's no way to guess what "apply sym_not_equal" means. But if you step through the proof line-by-line in the editor, then you can examine how each step updates your "proof goals". (I have an old blog post that shows what this looks like: http://www.randomhacks.net/2015/07/19/proving-sorted-lists-correct-using-coq-proof-assistent/ http://www.randomhacks.net/2015/07/19/proving-sorted-lists-c...) I admit, it can still be pretty arcane. But with the right tools and a bit of experience, it does get a lot easier. The real head-scratcher are advanced "proof tactics" like "auto", which automatically apply a long lists of possible transformations until they find an answer: Theorem basic_conj' : forall (A B : Prop), A -> B -> A /\ B. Proof. auto. Qed. This is the Coq version of "the proof is left as a exercise for the computer." It's pretty cool technology if you like math, well worth some time to puzzle it out. But expect to have to read some tutorials and think about them.

gus_massa 8y ago

> I don't, I know a proof but none including (3 . q - 2 . p). It's weird. I'm still looking at it. It would be nice to have an explanation here by someone that is a Coq specialist. Anyway, in a google search found this other proof that uses that > The last digit of the square of any positive integer written in base 3 can not be 2. [near a reference to Robert Gauntt] http://www.mathpath.org/proof/sqrt2.irrat.htm http://www.mathpath.org/proof/sqrt2.irrat.htm I'm not sure that it is related, but the 3q-2p and 3p-4q look like something that can be related to base 3. It looks like the base 3 proof doesn't use the Fundamental Theorem of Arithmetic, that is a very powerful result and I'm not sure if they have already a formal demonstration of that in Coq.