
{- some general logical concepts and principles -}

rel (A::Set) :: Type
  = A -> A -> Set

pred (A::Set) :: Type
  = A -> Set

exists :: (A::Set) -> (B::A -> Set) -> Set
  = \(A::Set) -> \(B::(x::A) -> Set) -> data Witness (u::A) (v::B u)

existsElim (A::Set)(B::A -> Set)(C::Set)
  :: (h1::exists A B) -> (h2::(x::A) -> B x -> C) -> C
  = \(h1::exists A B) ->
    \(h2::(x::A) -> (x'::B x) -> C) ->
    case h1 of { (Witness u v) -> h2 u v;}

and (A::Set)(B::Set) :: Set
  = data Pair (a::A) (b::B)

andElimLeft (A::Set)(B::Set) :: and A B -> A
  = \(h::and A B) -> case h of { (Pair a b) -> a;}

andElimRight (A::Set)(B::Set) :: and A B -> B
  = \(h::and A B) -> case h of { (Pair a b) -> b;}

or (A::Set)(B::Set) :: Set
  = data Inl (a::A) | Inr (b::B)

orElim (A::Set)(B::Set)(C::Set) :: (A -> C) -> (B -> C) -> or A B -> C
  = \(h1::(x::A) -> C) ->
    \(h2::(x::B) -> C) ->
    \(h3::or A B) ->
    case h3 of {
      (Inl a) -> h1 a;
      (Inr b) -> h2 b;}

noether (A::Set)(R::rel A) :: Type
  = (P::pred A) -> ((x::A) -> ((y::A) -> R y x -> P y) -> P x) -> (x::A) -> P x

N0 :: Set
  = data 

not (A::Set) :: Set
  = A -> N0

{- The principle of infinite descent, following Fermat -}


infiniteDescent (A::Set)
                (R::rel A)
                (P::pred A)
  :: noether A R -> 
     ((x::A) -> P x -> exists A (\(x1::A) -> and (R x1 x) (P x1))) -> 
     (x::A) -> not (P x)
  = \ (h1::noether A R) -> 
    \ (h2::(x::A) -> P x -> exists A (\(x1::A) -> and (R x1 x) (P x1))) -> 
    \ (x::A) -> 
    h1 (\(y::A) -> not (P y))
       (\(z::A) ->
        \(h3::(y::A) -> (x'::R y z) -> not (P y)) ->
        \(h4::P z) ->
        existsElim A (\(x1::A) -> and (R x1 z) (P x1)) N0 (h2 z h4)
         (\(y::A) ->
          \(h5::and (R y z) (P y)) ->
          h3 y (andElimLeft (R y z) (P y) h5) (andElimRight (R y z) (P y) h5)))
      x
{-# Alfa hiding on
var "not" as "#" with symbolfont
var "existsElim" hide 3
var "or" infix 0 as "#" with symbolfont
var "orElim" hide 3
var "and" infix 0 as "#" with symbolfont
var "andElimLeft" hide 2
var "andElimRight" hide 2
var "N0" as "^" with symbolfont
 #-}


--#include "noether.alfa"

{- Definition of commutative monoid; for the main proof, it 
   will be the monoid N* for multiplication -}

AbMonoid (A::Set)(eq::rel A) :: Set
  = sig {ref :: (x::A) -> eq x x;
         sym :: (x::A) -> (y::A) -> eq x y -> eq y x;
         trans :: (x::A) -> (y::A) -> (z::A) -> eq x y -> eq y z -> eq x z;
         ss :: A -> A -> A;
         cong ::
           (x1::A) ->
           (x2::A) ->
           (y1::A) ->
           (y2::A) ->
           eq x1 x2 -> eq y1 y2 -> eq (ss x1 y1) (ss x2 y2);
         assoc :: (x::A) -> (y::A) -> (z::A) -> eq (ss x (ss y z)) (ss (ss x y) z);
         comm :: (x::A) -> (y::A) -> eq (ss x y) (ss y x);}

{- A beginning of the theory of commutative monoid -}

package ThAbMonoid (A::Set)(eq::rel A)(m::AbMonoid A eq)  where
  open m  use  ref,  sym,  trans,  cong,  ss,  assoc,  comm
  square (x::A) :: A
    = ss x x
  multiple (p::A) :: rel A
    = \(x::A) -> \(y::A) -> eq (ss p x) y
  congLeft (x::A)(y::A)(z::A) :: eq y z -> eq (ss y x) (ss z x)
    = \(h::eq y z) -> cong y z x x h (ref x)
  congRight (x::A)(y::A)(z::A) :: eq y z -> eq (ss x y) (ss x z)
    = \(h::eq y z) -> cong x x y z (ref x) h
  lemma0 (x::A)(y::A)(z::A) :: eq x z -> eq y z -> eq x y
    = \(h::eq x z) -> \(h'::eq y z) -> trans x z y h (sym y z h')
  lemma2 (x::A)(y::A) :: eq x y -> eq (square x) (square y)
    = \(h::eq x y) -> cong x y x y h h
  lemma3 (x::A)(y::A)(z::A) :: eq (ss x (ss y z)) (ss y (ss x z))
    = lemma0 (ss x (ss y z)) (ss y (ss x z)) (ss (ss x y) z) (assoc x y z)
        (trans (ss y (ss x z)) (ss (ss y x) z) (ss (ss x y) z) (assoc y x z)
           (congLeft z (ss y x) (ss x y) (comm y x)))
  lemma4 (x::A)(y::A) :: eq (ss x (ss x (square y))) (square (ss x y))
    = trans (ss x (ss x (square y))) (ss x (ss y (ss x y))) (square (ss x y))
        (congRight x (ss x (square y)) (ss y (ss x y)) (lemma3 x y y))
        (assoc x y (ss x y))
  lemma5 (p::A)(y::A)(y1::A)
    :: eq (ss p y1) y -> eq (ss p (ss p (square y1))) (square y)
    = \(h::multiple p y1 y) ->
      trans (ss p (ss p (square y1))) (square (ss p y1)) (square y) (lemma4 p y1)
        (lemma2 (ss p y1) y h)
{-# Alfa hiding on
var "square"
var "trans" hide 3
var "cong" hide 4
var "assoc" hide 3
var "comm" hide 2
var "lemma0" hide 3
var "lemma3" hide 3
var "lemma2" hide 2
var "congLeft" hide 3
var "congRight" hide 3
var "lemma4" hide 2
var "lemma5" hide 3
var "eq" infix 0 as "=="
var "ss" infix 0 as " " with symbolfont
 #-}


--#include "lem.alfa"

{- Cancelative abelian monoid; N* is cancelative
   for the multiplication -}

isCancel (A::Set)(eq::rel A)(m::AbMonoid A eq) :: Set
  = (x::A) -> (y::A) -> (z::A) -> eq (m.ss z x) (m.ss z y) -> eq x y

package square
  (A::Set)(eq::rel A)(m::AbMonoid A eq)(cancel::isCancel A eq m)
 where
  open m  use  ref,  sym,  trans,  cong,  ss,  assoc,  comm
  open ThAbMonoid A eq m  use  square,  multiple
  lemma1 (p::A)(u::A)(v::A)(w::A) :: eq (ss p u) w -> eq (ss p v) w -> eq u v
    = \(h2::multiple p u w) ->
      \(h3::multiple p v w) ->
      cancel u v p ((ThAbMonoid A eq m).lemma0 (ss p u) (ss p v) w h2 h3)
  lemma2 (p::A)(x::A)(y::A)(y1::A)
    :: eq (ss p (square x)) (square y) ->
       eq (ss p y1) y -> eq (ss p (square y1)) (square x)
    = \(h1::multiple p (square x) (square y)) ->
      \(h2::multiple p y1 y) ->
      lemma1 p (ss p (square y1)) (square x) (square y)
        ((ThAbMonoid A eq m).lemma5 p y y1 h2)
        h1
  exA :: pred A -> Set
    = exists A
  divides :: rel A
    = \(x::A) -> \(y::A) -> exA (\(z::A) -> eq (ss x z) y)
  prime :: pred A
    = \(p::A) ->
      (x::A) ->
      (y::A) ->
      divides p (ss x y) -> or (divides p x) (divides p y)
  lemma3 (p::A)(x::A) :: prime p -> divides p (square x) -> divides p x
    = \(h1::prime p) ->
      \(h2::divides p (square x)) ->
      orElim (divides p x) (divides p x) (divides p x) (\(h::divides p x) -> h)
        (\(h::divides p x) -> h)
        (h1 x x h2)
  lemma4 (p::A)(x::A)(y::A)
    :: prime p ->
       eq (ss p (square x)) (square y) ->
       exA (\(y1::A) -> and (eq (ss p y1) y) (eq (ss p (square y1)) (square x)))
    = \(h1::prime p) ->
      \(h2::multiple p (square x) (square y)) ->
      let rem :: divides p y
            = lemma3 p y h1 (Witness@_ (square x) h2)
      in  existsElim A (\(z::A) -> eq (ss p z) y)
            (exA (\(y1::A) -> and (eq (ss p y1) y) (eq (ss p (square y1)) (square x))))
            rem
            (\(y1::A) ->
             \(h3::multiple p y1 y) ->
             Witness@_ y1 (Pair@_ h3 (lemma2 p x y y1 h2 h3)))
  Square :: rel A
    = \(p::A) -> \(x::A) -> exA (\(y::A) -> eq (ss p (square x)) (square y))
  lemma5 (p::A)(h2::prime p)(x::A)(h3::Square p x)
    :: exA (\(x1::A) -> and (eq (ss p x1) x) (Square p x1))
    = existsElim A (\(y::A) -> eq (ss p (square x)) (square y))
        (exA (\(x1::A) -> and (eq (ss p x1) x) (Square p x1)))
        h3
        (\(y::A) ->
         \(h4::multiple p (square x) (square y)) ->
         existsElim A
           (\(y1::A) -> and (eq (ss p y1) y) (eq (ss p (square y1)) (square x)))
           (exA (\(x1::A) -> and (eq (ss p x1) x) (Square p x1)))
           (lemma4 p x y h2 h4)
           (\(y1::A) ->
            \(h5::and (multiple p y1 y) (multiple p (square y1) (square x))) ->
            let mutual rem1 :: eq (ss p y1) y
                         = andElimLeft (multiple p y1 y) (multiple p (square y1) (square x)) h5
                       rem2 :: eq (ss p (square y1)) (square x)
                         = andElimRight (multiple p y1 y) (multiple p (square y1) (square x)) h5
            in  existsElim A
                  (\(y1'::A) -> and (multiple p y1' x) (multiple p (square y1') (square y1)))
                  (exA (\(x1::A) -> and (eq (ss p x1) x) (Square p x1)))
                  (lemma4 p y1 x h2 rem2)
                  (\(x1::A) ->
                   \(h6::and (multiple p x1 x) (multiple p (square x1) (square y1))) ->
                   let mutual rem3 :: eq (ss p x1) x
                                = andElimLeft (multiple p x1 x) (multiple p (square x1) (square y1))
                                    h6
                              rem4 :: eq (ss p (square x1)) (square y1)
                                = andElimRight (multiple p x1 x)
                                    (multiple p (square x1) (square y1))
                                    h6
                   in  Witness@_ x1 (Pair@_ rem3 (Witness@_ y1 rem4)))))
  isNotSquare :: pred A
    = \(p::A) -> (x::A) -> (y::A) -> not (eq (ss p (square x)) (square y))
  theorem (p::A) :: prime p -> noether A (multiple p) -> isNotSquare p
    = \(h1::prime p) ->
      \(h2::noether A (multiple p)) ->
      let rem :: (x::A) -> not (Square p x)
            = infiniteDescent A (multiple p) (Square p) h2 (lemma5 p h1)
      in  \(x::A) ->
          \(y::A) ->
          \(h3::eq (ss p (square x)) (square y)) ->
          rem x (Witness@_ y h3)

{- This is the main result; it applies to the case where A is
   N* and p is 2, but it shows as well that any prime cannot
   be a square of a rational 
-}
{-# Alfa hiding on
var "square"
var "trans" hide 3
var "cong" hide 4
var "assoc" hide 3
var "comm" hide 2
var "congLeft" hide 3
var "congRight" hide 3
var "lemma3" hide 2
var "lemma2" hide 4
var "lemma4" hide 3
var "lemma5" hide 1
var "exA" quantifier domain off as "$" with symbolfont
var "eq" infix 0 as "=="
var "ss" infix 0 as " " with symbolfont
var "lemma1" hide 4
var "divides" infix 0 as "|" with symbolfont
 #-}