(* ========================================================================= *)
(*                                                                           *)
(* * TEORIA DEI GRUPPI                                                       *)
(*                                                                           *)
(* ========================================================================= *)

(* ------------------------------------------------------------------------- *)
(* Comandi di base:                                                          *)
(*   Section XYZ. ...  End XYZ.   Aprire/chiudere una sezione                *)
(*   Variable X : T.              Dichiarare una variabile                   *)
(*   Hypothesis H : A.            Dichiarare una ipotesi                     *)
(*                                                                           *)
(* Tattiche:                                                                 *)
(*   reflexivity                  dimostra  x=x                              *)
(*   symmetry                     usando y=x dimostra x=y                    *)
(*   transitivity x               usando a=x e x=b dimostra a=b              *)
(*   rewrite H                    riscrivere una equazione                   *)
(* ------------------------------------------------------------------------- *)

Section Group.

Variable G : Set.               (* L'insieme "supporto" del gruppo.          *)
Variable op : G -> G -> G.      (* Il prodotto su  G.                        *)
Variable id : G.                (* L'identita' di G.                         *)
Variable iv : G -> G.           (* L'inverso.                                *)

(* ------------------------------------------------------------------------- *)
(* Supponiamo di avere le tre proprieta' essenziali:                         *)
(*  - associativa,                                                           *)
(*  - identita' a sinistra,                                                  *)
(*  - inverso a sinistra.                                                    *)
(* NB: siccome il nostro operato `op' non e' un simbolo infisso, dobbiamo    *)
(* scrivere `op x y' invece di `x op y' (oppure `x * y' oppure `x y' etc).   *)
(* ------------------------------------------------------------------------- *)

Hypothesis assoc : forall x y z : G, op x (op y z) = op (op x y) z.
Hypothesis id_left : forall x : G, op id x = x.
Hypothesis iv_left : forall x : G, op (iv x) x = id.

(* ------------------------------------------------------------------------- *)
(* Lemma di cancellazione:                                                   *)
(*   op x y = op x z -> y = z.                                               *)
(* Idea della dimostrazione:                                                 *)
(*   y = id * y = inv x * x * y = inv x * x * z = id z = z                   *)
(* Piu' dettagliatamente, con le nostre notazioni e usando esplicitamente la *)
(* proprieta' associativa, la catana di uguaglianze da usare e':             *)
(*   y = op id y = op (op (iv x) x) y = op (iv x) (op x y) =                 *)
(*       op (iv x) (op x z) = op (op (iv x) x) z = op id z = z               *)
(* ------------------------------------------------------------------------- *)

Lemma cancel : forall x y z : G,
  op x y = op x z -> y = z.
intros.
transitivity (op (op (iv x) x) y).
rewrite iv_left.
rewrite id_left.
reflexivity.
rewrite <-  assoc.
rewrite H.
rewrite assoc.
rewrite iv_left.
rewrite id_left.
reflexivity.
Qed.

(* ------------------------------------------------------------------------- *)
(* Tra gli assiomi (le Hypothesis all'inizio della sezione) non abbiamo      *)
(* supposto la proprieta' dell'identita' a destra perche' puo' essere        *)
(* facilmente dimostrata in questo modo:                                     *)
(* Per ogni x si ha                                                          *)
(*   op x (op id x) = (op x id) x = x * x                                    *)
(* e usando il lemma di cancellazione all'equazione precedente si ha         *)
(*    op id x = x                                                            *)
(* ------------------------------------------------------------------------- *)

Lemma id_right : forall x : G, op x id = x.
intros.
(* Adesso vogliamo usare il lemma di cancellazione.                         *)
(* Usiamo apply, ma dobbimo speficare con quale "x" (perche'?)              *)
apply cancel with (x := iv x).
rewrite assoc.
rewrite iv_left.
rewrite id_left.
reflexivity.
Qed.

(* ------------------------------------------------------------------------- *)
(* Esercizio: Anche la proprieta' dell'inverso a destra puo' essere          *)
(* facilmente dimostrata in modo analogo.  Si provi a scrivere la            *)
(* dimostrazione su carta prima di eseguire la seguente dimostrazione Coq.   *)
(* ------------------------------------------------------------------------- *)

Lemma iv_right : forall x : G, op x (iv x) = id.

Qed.

(* ------------------------------------------------------------------------- *)
(* Esercizio.                                                                *)
(* ------------------------------------------------------------------------- *)

Lemma iv_id : iv id = id.

Qed.

(* ------------------------------------------------------------------------- *)
(* Esercizio*.                                                               *)
(* ------------------------------------------------------------------------- *)

Lemma iv_iv : forall x : G, iv (iv x) = x.

Qed.

(* ------------------------------------------------------------------------- *)
(* Esercizio*.                                                               *)
(* ------------------------------------------------------------------------- *)

Lemma iv_op : forall x y : G, iv (op x y) = op (iv y) (iv x).

Qed.

(* ------------------------------------------------------------------------- *)
(* Adesso dimostriamo che ogni gruppo di ordine due (cioe' il quadrato di    *)
(* ogni elemento e' l'identita') e' abeliano.  Siccome abbiamo bisogno di    *)
(* una nuova ipotesi, lo facciamo in una sottosezione che chiamiamo Ord2     *)
(* ------------------------------------------------------------------------- *)

(* ------------------------------------------------------------------------- *)
(* Esercizio: Dopo aver eseguito e capito le seguenti due dimostrazioni,     *)
(* provare a trascriverle su carta.                                          *)
(* ------------------------------------------------------------------------- *)

Section Ord2.

Hypothesis ord2 : forall x : G, op x x = id.   (* G ha ordine 2 *)

(* ------------------------------------------------------------------------- *)
(* In un gruppo di ordine due, ogni elemento e' l'inverso di se stesso.      *)
(* ------------------------------------------------------------------------- *)

Lemma ord2_iv : forall x, iv x = x.

Qed.

Lemma ord2_comm : forall x y, op x y = op y x.

Qed.

End Ord2.

End Group.