(* dans le commentaire ci-dessous,placer le curseur entre la parenthèse fermante après
cl_extra, et le "*" puis faire ctrl x - ctrl e pour lancer proof-general*)

(* (load-library "cl-extra") *)

Section fractions_entiers_naturels.

  Inductive Fraction: Set:=
    |frac: nat -> nat -> Fraction.

  Inductive f_eq: Fraction -> Fraction -> Prop:=
  |f_refl: forall x:Fraction, f_eq x x
  |f_sym: forall x y:Fraction, f_eq x y -> f_eq y x
  |f_trans: forall x y z:Fraction, f_eq x y -> f_eq y z -> f_eq x z
  |f_eq_prod: forall a b c:nat,
      b<>0 -> c<>0 -> f_eq (frac a b) (frac (a * c) (b * c)).

  Definition f_somme (x y:Fraction):=
    match x with
    | frac a b => match y with
                    |frac c d => frac ((a * d)+(b * c)) (b*d)
                    end
    end.

  Theorem eq_zeitnot: f_eq (f_somme (frac 2 7) (frac 3 7)) (frac 5 7).
  Proof.
    simpl.
    apply f_sym.
    apply f_eq_prod with (c:=7).
    discriminate.
    discriminate.
  Qed.

  Definition numerateur (p:Fraction):nat:=match p with | frac a b => a end.
  Definition denominateur (p:Fraction):nat:=match p with | frac a b => b end.

  Section propriétés_des_entiers.

    Theorem plus_comm: forall p q:nat, p + q = q + p.
    Proof.
      induction p.
      intros.
      simpl.
      rewrite <- plus_n_O.
      reflexivity.
      intros.
      rewrite <- plus_n_Sm.
      simpl.
      rewrite IHp.
      reflexivity.
    Qed.

    Theorem plus_asso: forall p q r:nat, (p + q) + r = p + (q + r).
    Proof.
      induction p.
      intros.
      simpl.
      reflexivity.
      intros.
      rewrite plus_Sn_m.
      rewrite plus_Sn_m.
      rewrite plus_Sn_m.
      rewrite IHp.
      reflexivity.
    Qed.

    Theorem distributivite_droite: forall x y z:nat, (x+y)*z = (x*z)+(y*z).
    Proof.
      induction x.
      simpl.
      reflexivity.
      simpl.
      intros.
      assert (z+  x * z + y * z = z + (x * z + y * z)).
      apply  plus_asso.
      rewrite H.
      apply f_equal.
      apply IHx.
    Qed.

    Theorem mult_comm: forall x y:nat, x*y = y*x.
    Proof.
      induction x.
      simpl.
      intro.
      rewrite <- mult_n_O.
      reflexivity.
      simpl.
      assert (forall a b:nat, b * (S a) = b + b * a).
      induction b.
      simpl.
      reflexivity.
      simpl.
      rewrite IHb.
      apply f_equal.
      rewrite <- plus_asso.
      rewrite <- plus_asso.
      rewrite plus_comm with (p:=a) (q:=b).
      reflexivity.
      intro.
      apply eq_sym.
      rewrite IHx.
      apply H.
    Qed.

    Theorem mult_asso: forall x y z:nat, x*(y*z)=(x*y)*z.
    Proof.
      induction x.
      intros.
      simpl.
      reflexivity.
      simpl.
      intros.
      rewrite distributivite_droite.
      rewrite IHx.
      reflexivity.
    Qed.

    Theorem distributivite_gauche: forall x y z:nat, z*(x+y)= (z*x)+(z*y).
    Proof.
      intros.
      rewrite mult_comm with (x:=z) (y:= x+ y).
      rewrite mult_comm with (x:=z) (y:=x).
      rewrite mult_comm with (x:=z) (y:=y).
      apply distributivite_droite.
    Qed.

    Theorem un_neutre_mult: forall n:nat, n * 1 = n.
    Proof.
      induction n.
      simpl.
      reflexivity.
      simpl.
      rewrite IHn.
      reflexivity.
    Qed.

  End propriétés_des_entiers.

  Section propriétés_de_l'égalité_entre_fractions.

    Lemma nat_regulier: forall x y:nat, x<> 0 -> y <> 0 -> x*y <> 0.
    Proof.
      induction x.
      intros y Fairy.
      apply False_ind.
      apply Fairy.
      reflexivity.
      intros y NNSx NNy.
      simpl.
      destruct y.
      apply False_rect.
      apply NNy.
      reflexivity.
      simpl.
      discriminate.
    Qed.

    Lemma nat_regulier_2: forall p q r:nat, p+q = p+r -> q=r.
    Proof.
      induction p.
      intros p q.
      simpl.
      intro.
      assumption.
      intros q r.
      simpl.
      intro.
      apply IHp.
      apply eq_add_S.
      apply H.
    Qed.

    Lemma nat_regulier_3: forall p q r:nat,
        p <> 0 -> q * p = r * p -> q = r.
    Proof.
      intro.
      induction q.
      intro r.
      simpl.
      intros.
      destruct r.
      reflexivity.
      apply False_rect.
      apply eq_sym in H0.
      apply nat_regulier with (x:= S r) (y:=p).
      discriminate.
      assumption.
      assumption.
      intros.
      destruct r.
      assert (0*p = 0) as E.
      simpl; reflexivity.
      rewrite E in H0.
      absurd (S q * p = 0).
      apply nat_regulier.
      discriminate.
      assumption.
      assumption.
      simpl in H0.
      apply nat_regulier_2 in H0.
      apply eq_S.
      apply IHq.
      assumption.
      assumption.
    Qed.

    Lemma consistance_den_non_nul: forall x y:Fraction,
      f_eq x y -> (denominateur x <> 0 <-> denominateur y <> 0).
    Proof.
      apply f_eq_ind.
      intro x.
      apply iff_refl.
      intros x y Exy Ixy.
      apply iff_sym.
      apply Ixy.
      intros x y z Exy Ixy Eyz.
      apply iff_trans.
      apply Ixy.
      intros a b c NNb NNc.
      simpl.
      split.
      intro NNb2.
      apply nat_regulier.
      apply NNb.
      apply NNc.
      intro NNbc.
      apply NNb.
    Qed.

    Theorem caracterisation_de_l_egalite:forall a b c d:nat,
        b <> 0 -> d <> 0 ->
        (f_eq (frac a b) (frac c d) <-> a * d = b * c).
    Proof.
      intros a b c d Nb Nd.
      split.
      intro F.
      assert (let aux :=
                  fun (x y:Fraction) =>
                    denominateur x <> 0
                    -> denominateur y <> 0
                    -> (numerateur x) * (denominateur y) = (numerateur y) * (denominateur x)
              in
             forall p q:Fraction, f_eq p q -> aux p q)
        as L.
      apply f_eq_ind.
      intros.
      reflexivity.
      intros.
      apply eq_sym.
      apply H0.
      assumption.
      assumption.
      intros.
      assert (denominateur y <> 0) as Ny.
      apply consistance_den_non_nul with (x:=x).
      assumption.
      assumption.
      apply nat_regulier_3 with (p:= denominateur y).
      assumption.
      rewrite mult_comm with (x:= numerateur x * denominateur z) (y:= denominateur y).
      rewrite mult_asso.
      rewrite mult_comm with (x:= denominateur y) (y:= numerateur x).
      rewrite H0.
      rewrite <- mult_comm with (x:= denominateur x) (y:= numerateur y).
      rewrite <- mult_comm with (x:= denominateur x) (y:= numerateur z).
      rewrite <- mult_asso.
      rewrite <- mult_asso.
      rewrite H2.
      reflexivity.
      assumption.
      assumption.
      assumption.
      assumption.
      intros u v w.
      simpl.
      intros.
      rewrite <- mult_asso.
      rewrite mult_comm with (x:=v) (y:=w).
      reflexivity.
      simpl in L.
      assert (
          numerateur (frac a b) * denominateur (frac c d) =
          numerateur (frac c d) * denominateur (frac a b)
        ).
      apply L with (p:= frac a b) (q:= frac c d).
      assumption.
      simpl.
      assumption.
      simpl.
      assumption.
      simpl in H.
      rewrite mult_comm with (x:=b) (y:=c).
      assumption.
      intro.
      apply f_trans with (y:= frac (a * d) (b * d)).
      apply f_eq_prod.
      assumption.
      assumption.
      rewrite H.
      rewrite mult_comm with (x:=b) (y:=c).
      rewrite mult_comm with (x:=b) (y:=d).
      apply f_sym.
      apply f_eq_prod.
      assumption.
      assumption.
    Qed.

  End propriétés_de_l'égalité_entre_fractions.

  Section propriétés_arithmétiques_des_fractions.

  Theorem somme_fractions_de_meme_denominateur:
    forall a b c:nat,
      c <> 0 ->
      f_eq (f_somme (frac a c) (frac b c)) (frac (a+b) c).
  Proof.
    intros.
    simpl.
    rewrite mult_comm with (x:= c) (y:=b).
    rewrite <- distributivite_droite.
    apply f_sym.
    apply f_eq_prod.
    assumption.
    assumption.
  Qed.

  Definition f_produit (x y:Fraction):=
    match x with
    |frac a b => match y with
                 |frac c d => frac (a * c) (b * d)
                 end
    end.

  Definition f_inverse (x:Fraction):=
    match x with
    |frac a b => frac b a
    end.

  Theorem identite_inverse: forall x:Fraction,
      (numerateur x <> 0) -> (denominateur x <> 0) ->
      f_eq (f_produit x (f_inverse x)) (frac 1 1).
  Proof.
    intro x.
    destruct x as (a,b).
    intros.
    simpl.
    rewrite mult_comm with (x:=a) (y:=b).
    apply f_sym.
    assert (frac (b*a) (b*a) = frac ((b * a) * 1) ((b * a) * 1)).
    rewrite (un_neutre_mult).
    reflexivity.
    rewrite H1.
    rewrite mult_comm with (x:= b * a) (y:=1).
    apply f_eq_prod.
    discriminate.
    apply nat_regulier.
    simpl in H0.
    assumption.
    simpl in H.
    assumption.
  Qed.

  Theorem somme_fractions_associative: forall x y z:Fraction,
      f_eq (f_somme (f_somme x y) z)
           (f_somme x (f_somme y z)).
  Proof.
    intros x y z.
    destruct x as (a,b).
    destruct y as (c,d).
    destruct z as (e,f).
    simpl.
    assert ((a * d + b * c) * f + b * d * e = a * (d * f) + b * (c * f + d * e)).
    apply eq_trans with (y:= a * d * f + b * c *f + b * d * e).
    rewrite distributivite_droite.
    reflexivity.
    rewrite mult_asso with (x:=a) (y:=d) (z:=f).
    rewrite plus_asso with (p:=a * d * f) (q:= b * c * f) (r:= b * d * e).
    rewrite distributivite_gauche with (x:= c * f) (y:= d * e) (z:= b).
    rewrite mult_asso with (x:=b) (y:=c) (z:=f).
    rewrite mult_asso with (x:=b) (y:=d) (z:=e).
    reflexivity.
    rewrite H.
    rewrite mult_asso with (x:=b) (y:=d) (z:=f).
    apply f_refl.
  Qed.

  Theorem fractions_distributivite_droite: forall x y z:Fraction,
      denominateur x <> 0 ->
      denominateur y <> 0 ->
      denominateur z <> 0 ->
      f_eq (f_produit (f_somme x y) z)
           (f_somme (f_produit x z) (f_produit y z)).
  Proof.
    intros x y z.
    destruct x as (a,b).
    destruct y as (c,d).
    destruct z as (e,f).
    simpl.
    rewrite mult_asso with (x:= b * f) (y:=d) (z:=f).
    assert (((a * d + b * c) * e) * f = (a * e * (d * f) + b * f * (c * e))).
    rewrite distributivite_droite with (x:= a * d) (y:= b * c) (z := e).
    rewrite <- mult_asso with (x:= b) (y:=c) (z:=e).
    rewrite <- mult_asso with (x:= a) (y:=d) (z:=e).
    rewrite mult_comm with (x:=d) (y:=e).
    rewrite mult_asso with (x:= a) (y:=e) (z:=d).
    rewrite distributivite_droite with (x:= a * e * d) (y:= b * (c * e)) (z := f).
    rewrite mult_asso with (x:= a * e) (y:=d) (z:=f).
    rewrite <- mult_asso with (x:= b) (y:=f) (z:=c * e).
    rewrite mult_comm with (x:=f) (y:=c * e).
    rewrite mult_asso with (x:= b) (y:=c * e) (z:=f).
    reflexivity.
    rewrite <- H.
    intros.
    rewrite <- mult_asso with (x:= b) (y:=f) (z:=d).
    rewrite mult_comm with (x:=f) (y:=d).
    rewrite mult_asso with (x:= b) (y:=d) (z:=f).
    apply f_eq_prod.
    apply nat_regulier.
    apply nat_regulier.
    assumption.
    assumption.
    assumption.
    assumption.
  Qed.

  Theorem somme_fractions_commutative:
    forall x y:Fraction,
      f_eq (f_somme x y) (f_somme y x).
  Proof.
    intros x y.
    destruct x as (a,b).
    destruct y as (c,d).
    simpl.
    rewrite mult_comm with (x:=b) (y:=d).
    rewrite mult_comm with (x:=b) (y:=c).
    rewrite mult_comm with (x:=a) (y:=d).
    rewrite plus_comm with (p:=d * a) (q:=c * b).
    apply f_refl.
  Qed.

  Theorem produit_fractions_commutatif:
    forall x y:Fraction,
      f_eq (f_produit x y) (f_produit y x).
  Proof.
    intros x y.
    destruct x as (a,b).
    destruct y as (c,d).
    simpl.
    rewrite mult_comm with (x:=b) (y:=d).
    rewrite mult_comm with (x:=a) (y:=c).
    apply f_refl.
  Qed.

  Theorem produit_fractions_associatif: forall x y z:Fraction,
      f_eq (f_produit (f_produit x y) z)
           (f_produit x (f_produit y z)).
  Proof.
    intros x y z.
    destruct x as (a,b).
    destruct y as (c,d).
    destruct z as (e,f).
    simpl.
    rewrite mult_asso with (x:=a) (y:=c) (z:=e).
    rewrite mult_asso with (x:=b) (y:=d) (z:=f).
    apply f_refl.
  Qed.

  Theorem compatibility_f_eq_operations:
    forall x x' y y':Fraction,
      denominateur x <> 0 ->
      denominateur x' <> 0 ->
      denominateur y <> 0 ->
      denominateur y' <> 0 ->
      f_eq  x x' -> f_eq y y' -> (f_eq (f_somme x y) (f_somme x' y') /\
                                  f_eq (f_produit x y) (f_produit x' y')).
  Proof.
    assert (let aux := fun u v:Fraction =>
                         forall w:Fraction,denominateur w <> 0 ->
                           ((f_eq (f_somme u w) (f_somme v w))/\
                           (f_eq (f_produit u w) (f_produit v w)))
            in
            forall p q:Fraction, f_eq p q -> aux p q) as E.
    apply f_eq_ind.
    intros; split; apply f_refl; apply f_refl.
    intros x y F G w Nw;split; apply f_sym; apply G.
    assumption.
    assumption.
    intros x y z F G H K w Nw.
    split.
    apply f_trans with (y:= f_somme y w).
    apply G.
    assumption.
    apply K.
    assumption.
    apply f_trans with (y:= f_produit y w).
    apply G; assumption.
    apply K; assumption.
    intros a b c Nb Nc w Nw.
    destruct w as (e,f).
    simpl.
    assert (forall k m n:nat, k * m * n = k * n * m) as L.
    intros.
    rewrite <- mult_asso with (x:=k)(y:=m)(z:=n).
    rewrite <- mult_asso with (x:=k)(y:=n)(z:=m).
    rewrite mult_comm with (x:=m)(y:=n).
    reflexivity.
    rewrite L with (k:=a)(m:=c)(n:=e).
    rewrite L with (k:=a)(m:=c)(n:=f).
    rewrite L with (k:=b)(m:=c)(n:=e).
    rewrite L with (k:=b)(m:=c)(n:=f).
    split.
    rewrite <- distributivite_droite with (x:= a * f) (y:= b * e) (z:=c).
    apply f_eq_prod.
    simpl in Nw.
    apply nat_regulier.
    assumption.
    assumption.
    assumption.
    apply f_eq_prod.
    simpl in Nw.
    apply nat_regulier.
    assumption.
    assumption.
    assumption.
    intros; split.
    apply f_trans with (y:= f_somme x' y).
    apply E.
    assumption.
    assumption.
    apply f_trans with (y:= f_somme y x').
    apply somme_fractions_commutative.
    apply f_trans with (y:= f_somme y' x').
    apply E.
    assumption.
    assumption.
    apply somme_fractions_commutative.
    apply f_trans with (y:= f_produit x' y).
    apply E.
    assumption.
    assumption.
    apply f_trans with (y:= f_produit y x').
    apply produit_fractions_commutatif.
    apply f_trans with (y:= f_produit y' x').
    apply E.
    assumption.
    assumption.
    apply produit_fractions_commutatif.
  Qed.

  Theorem fractions_distributivite_gauche: forall x y z:Fraction,
      denominateur x <> 0 ->
      denominateur y <> 0 ->
      denominateur z <> 0 ->
      f_eq (f_produit z (f_somme x y))
           (f_somme (f_produit z x) (f_produit z y)).
  Proof.
    intros.
    apply f_trans with (y:= f_produit (f_somme x y) z).
    apply produit_fractions_commutatif.
    apply f_trans with (f_somme (f_produit x z) (f_produit y z)).
    apply fractions_distributivite_droite.
    assumption.
    assumption.
    assumption.
    destruct x as (a,b).
    destruct y as (c,d).
    destruct z as (e,f).
    simpl in H; simpl in H0; simpl in H1.
    apply compatibility_f_eq_operations.
    simpl.
    apply nat_regulier.
    assumption.
    assumption.
    simpl.
    apply nat_regulier.
    assumption.
    assumption.
    simpl.
    apply nat_regulier.
    assumption.
    assumption.
    simpl.
    apply nat_regulier.
    assumption.
    assumption.
    apply produit_fractions_commutatif.
    apply produit_fractions_commutatif.
  Qed.

  End propriétés_arithmétiques_des_fractions.

  Section Bonus_l'égalité_est_décidable.

    Fixpoint nat_eq_dec (m n:nat) {struct m}:sumbool (m = n)(m <> n).
    Proof.
      destruct m.
      destruct n.
      left.
      reflexivity.
      right.
      discriminate.
      destruct n.
      right.
      discriminate.
      destruct nat_eq_dec with (m:=m) (n:=n).
      left.
      apply eq_S.
      assumption.
      right.
      intro.
      apply n0.
      apply eq_add_S.
      assumption.
    Defined.

    Lemma caracterisation_eq_den_nul: forall x y:Fraction,
        f_eq x y -> (denominateur x = 0 -> denominateur y = 0 -> numerateur x = numerateur y).
    Proof.
      assert (let aux :=
                  fun x y:Fraction =>
                    (denominateur x = 0 -> denominateur y = 0 -> numerateur x = numerateur y)
              in
             forall p q:Fraction, f_eq p q -> aux p q)  as L.
      apply f_eq_ind.
      intros; reflexivity.
      intros.
      apply eq_sym.
      apply H0.
      assumption.
      assumption.
      intros.
      assert (denominateur y = 0 \/ denominateur y <> 0).
      destruct (denominateur y).
      left.
      reflexivity.
      right.
      discriminate.
      destruct H5.
      rewrite H0.
      apply H2.
      assumption.
      assumption.
      assumption.
      assumption.
      absurd (denominateur z = 0).
      apply consistance_den_non_nul with (x:=y).
      assumption.
      assumption.
      assumption.
      intros.
      simpl.
      simpl in H1.
      apply False_ind.
      apply H.
      apply H1.
      simpl in L.
      apply L.
    Qed.

    Definition f_eq_dec: forall x y:Fraction,
        sumbool (f_eq x y) (~f_eq x y).
    Proof.
      intros x y.
      destruct x as (a,b).
      destruct y as (c,d).
      destruct b.
      destruct d.
      destruct nat_eq_dec with (m:=a) (n:=c).
      rewrite e.
      left.
      apply f_refl.
      right.
      intro.
      apply caracterisation_eq_den_nul in H.
      simpl in H.
      apply n.
      apply H.
      simpl.
      reflexivity.
      simpl.
      reflexivity.
      right.
      intro.
      absurd (denominateur (frac a 0) = 0).
      apply consistance_den_non_nul with (x:= frac c (S d)).
      apply f_sym.
      assumption.
      simpl.
      discriminate.
      simpl.
      reflexivity.
      destruct d.
      right.
      intro.
      absurd (denominateur (frac c 0) = 0).
      apply consistance_den_non_nul with (x:= frac a (S b)).
      assumption.
      simpl.
      discriminate.
      simpl.
      reflexivity.
      destruct (nat_eq_dec (a * S d) (S b * c)).
      left.
      apply caracterisation_de_l_egalite.
      discriminate.
      discriminate.
      apply e.
      right.
      intro.
      apply n.
      apply caracterisation_de_l_egalite.
      discriminate.
      discriminate.
      assumption.
    Defined.

  End Bonus_l'égalité_est_décidable.

End fractions_entiers_naturels.