(**************************************************************************)
(*       ___	                                                          *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
(*      ||A||       E.Tassi, S.Zacchiroli                                 *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU Lesser General Public License Version 2.1         *)
(*                                                                        *)
(**************************************************************************)

(* Esercizio 0
   ===========

   Compilare i seguenti campi:

   Nome1: ...
   Cognome1: ...
   Matricola1: ...
   Account1: ...

   Nome2: ...
   Cognome2: ...
   Matricola2: ...
   Account2: ...

*)



include "nat/plus.ma".

lemma ex0: ∀n. n + O = n.
 assume n: nat.
 we proceed by induction on n to prove (n + O = n).
  case O.
   the thesis becomes (O + O = O).
    conclude
        (O + O)
      = O
    done.
  case S.
   assume n : nat.
   by induction hypothesis we know (n + O = n) (H).
   the thesis becomes (S n + O = S n).
    conclude
       (S n + O)
     = (S (n + O)).
     = (S n) by H
    done.
qed.

include "didactic/support/natural_deduction.ma".

definition Impl_elim_2: ∀A,B,C: CProp. (A ⇒ B ⇒ C) ⇒ A ⇒ B ⇒ C.
 intros; constructor 1. intro. cases H; constructor 1; intro.
 apply H1. assumption.
qed.

(* usare `apply rule (lem 3 Impl_elim_2 (A⇒B⇒C) (A) (B));` per la regola
  A ⇒ B ⇒ C      A       B
  ------------------------
             C
*)

(* Il nostro linguaggio del primo ordine prevede le seguenti 
   - costanti: O
   - funzioni: S (unaria), plus, mult (binarie)
   - predicati: eq (binari)
*)
axiom O : sort.                  (* zero *)
axiom S : sort → sort.           (* successore *)
axiom plus : sort → sort → sort. (* addizione *)
axiom mult: sort → sort → sort.  (* moltiplicazione *)
axiom eq : sort → sort → CProp.  (* uguaglianza *)

(*
notation < "+  term 90 x  term 90 y" non associative with precedence 80 for @{'plus $x $y}.
notation < "★  term 90 x  term 90 y" non associative with precedence 80 for @{'mult $x $y}.
notation < "=  term 90 x  term 90 y" non associative with precedence 80 for @{'eq $x $y}.
notation < "\S  term 90 x" non associative with precedence 80 for @{'S $x}.
notation < "\O" non associative with precedence 80 for @{'O}.
interpretation "O" 'O = O.
interpretation "S" 'S x y = (S x y).
interpretation "mult" 'mult x y = (mult x y).
interpretation "plus" 'plus x y = (plus x y).
interpretation "eq" 'eq x y = (eq x y).
*)

interpretation "+" 'my_plus x y = (plus x y). 
interpretation "*" 'my_mult x y = (mult x y).
interpretation "=" 'my_eq x y = (eq x y).
interpretation "S" 'my_S x = (S x).
interpretation "O" 'my_O = O.

notation "x + y" non associative with precedence 50 for @{'my_plus $x $y}.
notation "x * y" non associative with precedence 55 for @{'my_mult $x $y}.
notation "x = y" non associative with precedence 45 for @{'my_eq $x $y}.
notation > "'S' x" non associative with precedence 40 for @{'my_S $x}.
notation < "'S'  x" non associative with precedence 40 for @{'my_S $x}.
notation "'O'" non associative with precedence 90 for @{'my_O}.

(* Assumiamo la seguente teoria *)

(* l'uguaglianza e' una relazione d'equivalenza *)
axiom refl: ∀x. x = x.
axiom sym: ∀x.∀y. x = y ⇒ y = x.
axiom trans: ∀x.∀y.∀z. x = y ⇒ y = z ⇒ x = z.

(* assiomi di Peano *)
axiom discr: ∀x. ¬ O = (S x).
axiom inj: ∀x.∀y. (S x) = (S y) ⇒ x = y.
(* Questo è uno schema di assiomi: è come avere una regola di induzione per 
   ogni predicato unario P. Il sistema inferisce automaticamente P. *)  
axiom induct: ΠP : sort → CProp. P O ⇒ (∀n. P n ⇒ P (S n)) ⇒ ∀x.P x.

(* definizione ricorsiva di addizione *)
axiom plus_O: ∀x. O + x = x.
axiom plus_S: ∀x.∀y. (S x) + y = S (x + y).

(* definizione ricorsiva di moltiplicazione *)
axiom mult_O: ∀x.O * x = O.
axiom mult_S: ∀x.∀y. (S x) * y = x * y + y.

(* l'uguaglianza e' una congruenza rispetto a tutte le funzioni e predicati *)
axiom eq_S: ∀x.∀x'. x = x' ⇒ (S x) = (S x').
axiom eq_plus: ∀x.∀x'.∀y.∀y'. x = x' ⇒ y = y' ⇒ x + y = x' + y'.
axiom eq_mult: ∀x.∀x'.∀y.∀y'. x = x' ⇒ y = y' ⇒ x * y = x' * y'.


(* intuizionista *)
lemma ex1: ∀x.x + O = x.
apply rule (prove (∀x.x + O = x));
(* poichè tutti gli assiomi della teoria sono assiomi e non dimostrazioni,
   l'unica forma di `apply rule lem` che potete usare è 
   `apply rule (lem 0 nome_assioma)` *)
…
qed.