(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)


(*****************************************************************************)
(*          Projet Formel - Calculus of Inductive Constructions V5.10        *)
(*****************************************************************************)
(*									     *)
(*	               Free Monoid (Kleene Closure)                          *)
(*									     *)
(*****************************************************************************)
(*									     *)
(*                     A. SAIBI	  May 95                  		     *)
(*									     *)
(*****************************************************************************)

Require Export Monoid.

Set Implicit Arguments.
Unset Strict Implicit.

Section freem_def.

Variable A : Setoid.

Inductive Tlist : Type :=
  | Empty : Tlist
  | Concat1 : A -> Tlist -> Tlist.

Fixpoint Equal_Tlist (l : Tlist) : Tlist -> Prop :=
  fun m : Tlist =>
  match l, m with
  | Empty, Empty => True
  | Empty, _ => False
  | Concat1 a l1, Concat1 b m1 => a =_S b /\ Equal_Tlist l1 m1
  | _, _ => False
  end.

Lemma Equal_Tlist_equiv : Equivalence Equal_Tlist.
Proof.
(* Goal: @Equivalence Tlist Equal_Tlist *)
apply Build_Equivalence.
(* Goal: @Reflexive Tlist Equal_Tlist *)
(* Goal: @Partial_equivalence Tlist Equal_Tlist *)
unfold Reflexive in |- *; intro l; elim l; simpl in |- *.
(* Goal: Equal_Tlist (Concat t l1) (Concat t l2) *)
auto.
(* Goal: forall (c : Carrier A) (t : Tlist) (_ : Equal_Tlist t t), and (@Equal A c c) (Equal_Tlist t t) *)
(* Goal: @Partial_equivalence Tlist Equal_Tlist *)
intros; split; [ apply Refl | auto ].
(* Goal: @Partial_equivalence Tlist Equal_Tlist *)
apply Build_Partial_equivalence.
(* Goal: @Transitive Tlist Equal_Tlist *)
(* Goal: @Symmetric Tlist Equal_Tlist *)
unfold Transitive in |- *; intros l1; elim l1.
(* Goal: forall (a2 b : Carrier Tlist_setoid) (_ : @Equal Tlist_setoid Empty a2), @Equal Tlist_setoid (Concat Empty b) (Concat a2 b) *)
(* Goal: forall (c : Carrier A) (t : Tlist) (_ : forall (a2 b : Carrier Tlist_setoid) (_ : @Equal Tlist_setoid t a2), @Equal Tlist_setoid (Concat t b) (Concat a2 b)) (a2 b : Carrier Tlist_setoid) (_ : @Equal Tlist_setoid (Concat1 c t) a2), @Equal Tlist_setoid (Concat (Concat1 c t) b) (Concat a2 b) *)
intro l2; elim l2.
(* Goal: forall (z : Tlist) (_ : Equal_Tlist Empty Empty) (_ : Equal_Tlist Empty z), Equal_Tlist Empty z *)
(* Goal: forall (c : Carrier A) (t : Tlist) (_ : forall (z : Tlist) (_ : Equal_Tlist Empty t) (_ : Equal_Tlist t z), Equal_Tlist Empty z) (z : Tlist) (_ : Equal_Tlist Empty (Concat1 c t)) (_ : Equal_Tlist (Concat1 c t) z), Equal_Tlist Empty z *)
(* Goal: forall (c : Carrier A) (t : Tlist) (_ : forall (y z : Tlist) (_ : Equal_Tlist t y) (_ : Equal_Tlist y z), Equal_Tlist t z) (y z : Tlist) (_ : Equal_Tlist (Concat1 c t) y) (_ : Equal_Tlist y z), Equal_Tlist (Concat1 c t) z *)
(* Goal: @Symmetric Tlist Equal_Tlist *)
intro l3; elim l3; simpl in |- *; trivial.
(* Goal: forall (c : Carrier A) (t : Tlist) (_ : forall (z : Tlist) (_ : Equal_Tlist Empty t) (_ : Equal_Tlist t z), Equal_Tlist Empty z) (z : Tlist) (_ : Equal_Tlist Empty (Concat1 c t)) (_ : Equal_Tlist (Concat1 c t) z), Equal_Tlist Empty z *)
(* Goal: forall (c : Carrier A) (t : Tlist) (_ : forall (y z : Tlist) (_ : Equal_Tlist t y) (_ : Equal_Tlist y z), Equal_Tlist t z) (y z : Tlist) (_ : Equal_Tlist (Concat1 c t) y) (_ : Equal_Tlist y z), Equal_Tlist (Concat1 c t) z *)
(* Goal: @Symmetric Tlist Equal_Tlist *)
intros c t H z H1; elim H1.
(* Goal: forall (c : Carrier A) (t : Tlist) (_ : forall (y z : Tlist) (_ : Equal_Tlist t y) (_ : Equal_Tlist y z), Equal_Tlist t z) (y z : Tlist) (_ : Equal_Tlist (Concat1 c t) y) (_ : Equal_Tlist y z), Equal_Tlist (Concat1 c t) z *)
(* Goal: @Symmetric Tlist Equal_Tlist *)
intros c t H y; elim y.
(* Goal: forall (z : Tlist) (_ : Equal_Tlist (Concat1 c t) Empty) (_ : Equal_Tlist Empty z), Equal_Tlist (Concat1 c t) z *)
(* Goal: forall (c0 : Carrier A) (t0 : Tlist) (_ : forall (z : Tlist) (_ : Equal_Tlist (Concat1 c t) t0) (_ : Equal_Tlist t0 z), Equal_Tlist (Concat1 c t) z) (z : Tlist) (_ : Equal_Tlist (Concat1 c t) (Concat1 c0 t0)) (_ : Equal_Tlist (Concat1 c0 t0) z), Equal_Tlist (Concat1 c t) z *)
(* Goal: @Symmetric Tlist Equal_Tlist *)
intros z H1 H2; elim H1.
(* Goal: forall (c0 : Carrier A) (t0 : Tlist) (_ : forall (z : Tlist) (_ : Equal_Tlist (Concat1 c t) t0) (_ : Equal_Tlist t0 z), Equal_Tlist (Concat1 c t) z) (z : Tlist) (_ : Equal_Tlist (Concat1 c t) (Concat1 c0 t0)) (_ : Equal_Tlist (Concat1 c0 t0) z), Equal_Tlist (Concat1 c t) z *)
(* Goal: @Symmetric Tlist Equal_Tlist *)
intros c0 t0 H0 z; elim z.
(* Goal: forall (_ : Equal_Tlist (Concat1 c t) (Concat1 c0 t0)) (_ : Equal_Tlist (Concat1 c0 t0) Empty), Equal_Tlist (Concat1 c t) Empty *)
(* Goal: forall (c1 : Carrier A) (t1 : Tlist) (_ : forall (_ : Equal_Tlist (Concat1 c t) (Concat1 c0 t0)) (_ : Equal_Tlist (Concat1 c0 t0) t1), Equal_Tlist (Concat1 c t) t1) (_ : Equal_Tlist (Concat1 c t) (Concat1 c0 t0)) (_ : Equal_Tlist (Concat1 c0 t0) (Concat1 c1 t1)), Equal_Tlist (Concat1 c t) (Concat1 c1 t1) *)
(* Goal: @Symmetric Tlist Equal_Tlist *)
intros H1 H2; elim H2.
(* Goal: forall (c1 : Carrier A) (t1 : Tlist) (_ : forall (_ : Equal_Tlist (Concat1 c t) (Concat1 c0 t0)) (_ : Equal_Tlist (Concat1 c0 t0) t1), Equal_Tlist (Concat1 c t) t1) (_ : Equal_Tlist (Concat1 c t) (Concat1 c0 t0)) (_ : Equal_Tlist (Concat1 c0 t0) (Concat1 c1 t1)), Equal_Tlist (Concat1 c t) (Concat1 c1 t1) *)
(* Goal: @Symmetric Tlist Equal_Tlist *)
intros c1 t1 H1 H2 H3.
(* Goal: Equal_Tlist (Concat1 c t) (Concat1 c1 t1) *)
(* Goal: @Symmetric Tlist Equal_Tlist *)
elim H2; intros H4 H5.
(* Goal: Equal_Tlist (Concat1 c t) (Concat1 c1 t1) *)
(* Goal: @Symmetric Tlist Equal_Tlist *)
elim H3; intros H6 H7.
(* Goal: @Equal Tlist_setoid (Concat (Concat1 c t) l) (Concat (Concat1 c0 t0) l) *)
simpl in |- *; split.
(* Goal: @Equal A c c1 *)
(* Goal: Equal_Tlist t t1 *)
(* Goal: @Symmetric Tlist Equal_Tlist *)
apply Trans with c0; trivial.
(* Goal: Equal_Tlist t t1 *)
(* Goal: @Symmetric Tlist Equal_Tlist *)
apply (H t0 t1); trivial.
(* Goal: @Symmetric Tlist Equal_Tlist *)
unfold Symmetric in |- *; intro l1; elim l1.
(* Goal: forall (a2 b : Carrier Tlist_setoid) (_ : @Equal Tlist_setoid Empty a2), @Equal Tlist_setoid (Concat Empty b) (Concat a2 b) *)
(* Goal: forall (c : Carrier A) (t : Tlist) (_ : forall (a2 b : Carrier Tlist_setoid) (_ : @Equal Tlist_setoid t a2), @Equal Tlist_setoid (Concat t b) (Concat a2 b)) (a2 b : Carrier Tlist_setoid) (_ : @Equal Tlist_setoid (Concat1 c t) a2), @Equal Tlist_setoid (Concat (Concat1 c t) b) (Concat a2 b) *)
intro l2; elim l2.
(* Goal: Equal_Tlist t (Concat t Empty) *)
trivial.
(* Goal: forall (c : Carrier A) (t : Tlist) (_ : forall _ : Equal_Tlist Empty t, Equal_Tlist t Empty) (_ : Equal_Tlist Empty (Concat1 c t)), Equal_Tlist (Concat1 c t) Empty *)
(* Goal: forall (c : Carrier A) (t : Tlist) (_ : forall (y : Tlist) (_ : Equal_Tlist t y), Equal_Tlist y t) (y : Tlist) (_ : Equal_Tlist (Concat1 c t) y), Equal_Tlist y (Concat1 c t) *)
intros c t H H1; elim H1.
(* Goal: forall (c : Carrier A) (t : Tlist) (_ : forall (a2 b : Carrier Tlist_setoid) (_ : @Equal Tlist_setoid t a2), @Equal Tlist_setoid (Concat t b) (Concat a2 b)) (a2 b : Carrier Tlist_setoid) (_ : @Equal Tlist_setoid (Concat1 c t) a2), @Equal Tlist_setoid (Concat (Concat1 c t) b) (Concat a2 b) *)
intros c t H l2; elim l2.
(* Goal: Equal_Tlist t (Concat t Empty) *)
simpl in |- *; trivial.
(* Goal: forall (c0 : Carrier A) (t0 : Tlist) (_ : forall _ : Equal_Tlist (Concat1 c t) t0, Equal_Tlist t0 (Concat1 c t)) (_ : Equal_Tlist (Concat1 c t) (Concat1 c0 t0)), Equal_Tlist (Concat1 c0 t0) (Concat1 c t) *)
intros c0 t0 H0 H1.
(* Goal: Equal_Tlist (Concat1 c0 t0) (Concat1 c t) *)
elim H1; intros H2 H3.
(* Goal: @Equal Tlist_setoid (Concat (Concat1 c t) l) (Concat (Concat1 c0 t0) l) *)
simpl in |- *; split.
(* Goal: Equal_Tlist t (Concat t Empty) *)
apply Sym; trivial.
(* Goal: Equal_Tlist t (Concat t Empty) *)
apply H; trivial.
Qed.

Canonical Structure Tlist_setoid : Setoid := Equal_Tlist_equiv.

Fixpoint Concat (l : Tlist_setoid) : Tlist_setoid -> Tlist_setoid :=
  fun m : Tlist_setoid =>
  match l with
  | Empty => m
  | Concat1 a l1 => Concat1 a (Concat l1 m)
  end.

Lemma Diff_Concat1_Empty :
 forall (a : A) (l : Tlist), ~ Equal_Tlist (Concat1 a l) Empty.
Proof.
(* Goal: Equal_Tlist t (Concat t Empty) *)
unfold not in |- *; intros a l; simpl in |- *; trivial.
Qed.

Lemma Concat_congl : Map2_congl_law Concat.
Proof.
(* Goal: @Map2_congl_law Tlist_setoid Tlist_setoid Tlist_setoid Concat *)
unfold Map2_congl_law in |- *; intros l1 l2 l3.
(* Goal: forall _ : @Equal Tlist_setoid l1 l2, @Equal Tlist_setoid (Concat l3 l1) (Concat l3 l2) *)
elim l3; simpl in |- *.
(* Goal: Equal_Tlist t (Concat t Empty) *)
trivial.
(* Goal: forall (c : Carrier A) (t : Tlist) (_ : forall _ : Equal_Tlist l1 l2, Equal_Tlist (Concat t l1) (Concat t l2)) (_ : Equal_Tlist l1 l2), and (@Equal A c c) (Equal_Tlist (Concat t l1) (Concat t l2)) *)
intros c t H H0; split.
(* Goal: @Equal A c c *)
(* Goal: Equal_Tlist t (Concat t Empty) *)
apply Refl.
(* Goal: Equal_Tlist (Concat t l1) (Concat t l2) *)
auto.
Qed.

Lemma Concat_congr : Map2_congr_law Concat.
Proof.
(* Goal: @Map2_congr_law Tlist_setoid Tlist_setoid Tlist_setoid Concat *)
unfold Map2_congr_law in |- *; intro l1; elim l1.
(* Goal: forall (a2 b : Carrier Tlist_setoid) (_ : @Equal Tlist_setoid Empty a2), @Equal Tlist_setoid (Concat Empty b) (Concat a2 b) *)
(* Goal: forall (c : Carrier A) (t : Tlist) (_ : forall (a2 b : Carrier Tlist_setoid) (_ : @Equal Tlist_setoid t a2), @Equal Tlist_setoid (Concat t b) (Concat a2 b)) (a2 b : Carrier Tlist_setoid) (_ : @Equal Tlist_setoid (Concat1 c t) a2), @Equal Tlist_setoid (Concat (Concat1 c t) b) (Concat a2 b) *)
intro l2; elim l2.
(* Goal: @Equal A c c *)
(* Goal: Equal_Tlist t (Concat t Empty) *)
intros l H; apply Refl.
(* Goal: forall (c : Carrier A) (t : Tlist) (_ : forall (b : Carrier Tlist_setoid) (_ : @Equal Tlist_setoid Empty t), @Equal Tlist_setoid (Concat Empty b) (Concat t b)) (b : Carrier Tlist_setoid) (_ : @Equal Tlist_setoid Empty (Concat1 c t)), @Equal Tlist_setoid (Concat Empty b) (Concat (Concat1 c t) b) *)
(* Goal: forall (c : Carrier A) (t : Tlist) (_ : forall (a2 b : Carrier Tlist_setoid) (_ : @Equal Tlist_setoid t a2), @Equal Tlist_setoid (Concat t b) (Concat a2 b)) (a2 b : Carrier Tlist_setoid) (_ : @Equal Tlist_setoid (Concat1 c t) a2), @Equal Tlist_setoid (Concat (Concat1 c t) b) (Concat a2 b) *)
intros c t H l3 H1; elim H1.
(* Goal: forall (c : Carrier A) (t : Tlist) (_ : forall (a2 b : Carrier Tlist_setoid) (_ : @Equal Tlist_setoid t a2), @Equal Tlist_setoid (Concat t b) (Concat a2 b)) (a2 b : Carrier Tlist_setoid) (_ : @Equal Tlist_setoid (Concat1 c t) a2), @Equal Tlist_setoid (Concat (Concat1 c t) b) (Concat a2 b) *)
intros c t H l2; elim l2.
(* Goal: forall (b : Carrier Tlist_setoid) (_ : @Equal Tlist_setoid (Concat1 c t) Empty), @Equal Tlist_setoid (Concat (Concat1 c t) b) (Concat Empty b) *)
(* Goal: forall (c0 : Carrier A) (t0 : Tlist) (_ : forall (b : Carrier Tlist_setoid) (_ : @Equal Tlist_setoid (Concat1 c t) t0), @Equal Tlist_setoid (Concat (Concat1 c t) b) (Concat t0 b)) (b : Carrier Tlist_setoid) (_ : @Equal Tlist_setoid (Concat1 c t) (Concat1 c0 t0)), @Equal Tlist_setoid (Concat (Concat1 c t) b) (Concat (Concat1 c0 t0) b) *)
intros l H1; absurd (Equal_Tlist (Concat1 c t) Empty).
(* Goal: not (Equal_Tlist (Concat1 c t) Empty) *)
(* Goal: Equal_Tlist (Concat1 c t) Empty *)
(* Goal: forall (c0 : Carrier A) (t0 : Tlist) (_ : forall (b : Carrier Tlist_setoid) (_ : @Equal Tlist_setoid (Concat1 c t) t0), @Equal Tlist_setoid (Concat (Concat1 c t) b) (Concat t0 b)) (b : Carrier Tlist_setoid) (_ : @Equal Tlist_setoid (Concat1 c t) (Concat1 c0 t0)), @Equal Tlist_setoid (Concat (Concat1 c t) b) (Concat (Concat1 c0 t0) b) *)
apply Diff_Concat1_Empty.
(* Goal: Equal_Tlist t (Concat t Empty) *)
trivial.
(* Goal: Equal_Tlist (Concat1 c0 t0) (Concat1 c t) *)
intros c0 t0 H0 l H1; elim H1; intros H2 H3.
(* Goal: @Equal Tlist_setoid (Concat (Concat1 c t) l) (Concat (Concat1 c0 t0) l) *)
simpl in |- *; split.
(* Goal: Equal_Tlist t (Concat t Empty) *)
trivial.
(* Goal: Equal_Tlist t (Concat t Empty) *)
apply (H t0 l); trivial.
Qed.

Definition Concat_map2 := Build_Map2 Concat_congl Concat_congr.

Lemma Mass_FreeMonoid : Monoid_ass Concat_map2.
Proof.
(* Goal: @Monoid_ass Tlist_setoid Concat_map2 *)
unfold Monoid_ass in |- *; intros l m n; elim l.
(* Goal: @Equal A c c *)
(* Goal: Equal_Tlist t (Concat t Empty) *)
apply Refl.
(* Goal: forall (c : Carrier A) (t : Tlist) (_ : Equal_Tlist t (@Ap2 Tlist_setoid Tlist_setoid Tlist_setoid Concat_map2 t Empty)), and (@Equal A c c) (Equal_Tlist t (Concat t Empty)) *)
intros; split.
(* Goal: @Equal A c c *)
(* Goal: Equal_Tlist t (Concat t Empty) *)
apply Refl.
(* Goal: Equal_Tlist t (Concat t Empty) *)
trivial.
Qed.

Lemma Midl_FreeMonoid : Monoid_idl Concat_map2 Empty.
Proof.
(* Goal: @Monoid_idl Tlist_setoid Concat_map2 Empty *)
unfold Monoid_idl in |- *; intro l; elim l.
(* Goal: @Equal A c c *)
(* Goal: Equal_Tlist t (Concat t Empty) *)
apply Refl.
(* Goal: forall (c : Carrier A) (t : Tlist) (_ : Equal_Tlist t (@Ap2 Tlist_setoid Tlist_setoid Tlist_setoid Concat_map2 t Empty)), and (@Equal A c c) (Equal_Tlist t (Concat t Empty)) *)
intros; split.
(* Goal: @Equal A c c *)
(* Goal: Equal_Tlist t (Concat t Empty) *)
apply Refl.
(* Goal: Equal_Tlist t (Concat t Empty) *)
trivial.
Qed.

Lemma Midr_FreeMonoid : Monoid_idr Concat_map2 Empty.
Proof.
(* Goal: @Monoid_idr Tlist_setoid Concat_map2 Empty *)
unfold Monoid_idr in |- *; intro l; elim l; simpl in |- *.
(* Goal: Equal_Tlist t (Concat t Empty) *)
trivial.
(* Goal: forall (c : Carrier A) (t : Tlist) (_ : Equal_Tlist t (@Ap2 Tlist_setoid Tlist_setoid Tlist_setoid Concat_map2 t Empty)), and (@Equal A c c) (Equal_Tlist t (Concat t Empty)) *)
intros; split.
(* Goal: @Equal A c c *)
(* Goal: Equal_Tlist t (Concat t Empty) *)
apply Refl.
(* Goal: Equal_Tlist t (Concat t Empty) *)
trivial.
Qed.

Canonical Structure FreeMonoid :=
  Build_Monoid Mass_FreeMonoid Midl_FreeMonoid Midr_FreeMonoid.

End freem_def.

Coercion FreeMonoid : Setoid >-> Monoid.