The Coq mailing list

[Daniel de Rauglaudre <daniel.de_rauglaudre AT inria.fr>]

Hi,

This is absolutely miraculous. It works!
With the other answers, I thought that my formula was wrong.
But it is true? Wow!

Question: I was even not able to prove it with pen and paper!
How did nsatz do it? Is it possible to see its proof, except
by typing "Show Proof"?

On Sun, Sep 25, 2016 at 10:28:26PM +0200, Laurent Thery wrote:
> 
> Hi,
> 
> Using grobner basis it works:
> 
> Require Import Reals Nsatz.
> 
> Open Scope R_scope.
> 
> Section F.
> 
> Variables m11 m12 m13
>           m21 m22 m23
>           m31 m32 m33 : R.
> Hypothesis Hd :
>   m11 * m22 * m33 + m12 * m23 * m31 + m13 * m21 * m32 -
>   m31 * m22 * m13 - m32 * m23 * m11 - m33 * m21 * m12 = 1.
> 
> Variable   H1 : m11 ^2 + m21 ^2 + m31^2  = 1%R.
> Variable   H2 : m12 ^2 + m22 ^2 + m32^2  = 1%R.
> Variable   H3 : m13 ^2 + m23 ^2 + m33^2  = 1%R.
> Variable   H4 : m11 * m12 + m21 * m22 + m31 * m32 = 0%R.
> Variable   H5 : m11 * m12 + m21 * m23 + m31 * m33 = 0%R.
> Variable   H6 : m12 * m13 + m22 * m23 + m32 * m33 = 0%R.
> 
> Let x := m32 - m23.
> Let y := m13 - m31.
> Let z := m21 - m12.
> 
> 
> Lemma F1 : (m11 * x + m12 * y + m13 * z)   = x.
> Proof.
> simpl in H1, H2, H3.
> nsatz.
> Qed.
> 
> Lemma F2 : (m21 * x + m22 * y + m23 * z)   = y.
> Proof.
> simpl in H1, H2, H3.
> nsatz.
> Qed.
> 
> Lemma F3 : (m31 * x + m32 * y + m33 * z)   = z.
> Proof.
> simpl in H1, H2, H3.
> nsatz.
> Qed.
> 
> --
> Laurent

-- 
Daniel de Rauglaudre
http://pauillac.inria.fr/~ddr/