Require Import Setoid Morphisms.

Local Set Implicit Arguments.
Local Unset Strict Implicit.


Inductive Acz : Type :=
  Asup : A : Type, (A Acz) Acz.

Arguments Asup _ _ : clear implicits.

Definition s :=
  match s with
    Asup A f A
  end.

Definition s : ( s) Acz :=
  match s with
    Asup A f f
  end.

Arguments _ : clear implicits.

Fixpoint Aeq s t :=
  match s, t with
    Asup A f, Asup B g ( a, b, Aeq (f a) (g b)) ( b, a, Aeq (f a) (g b))
  end.

Lemma Aeq_ref s :
  Aeq s s.
Proof.
  induction s as [A f IH]. simpl. split.
  - intros a. exists a. now apply IH.
  - intros a. exists a. now apply IH.
Qed.


Lemma Aeq_ref' s t :
  s = t Aeq s t.
Proof.
  intros . apply Aeq_ref.
Qed.


Lemma Aeq_sym s t :
  Aeq s t Aeq t s.
Proof.
  revert t. induction s as [A f IH].
  intros [B g]. simpl. intros [ ]. split.
  - intros b. destruct ( b) as [a ]. exists a. now apply IH.
  - intros a. destruct ( a) as [b ]. exists b. now apply IH.
Qed.


Lemma Aeq_tra s t u :
  Aeq s t Aeq t u Aeq s u.
Proof.
  revert t u. induction s as [A f IH].
  intros [B g] [C h]. simpl. intros [ ] [ ]. split.
  - intros a. destruct ( a) as [b ]. destruct ( b) as [c ].
    exists c. now apply IH with (t := (g b)).
  - intros c. destruct ( c) as [b ]. destruct ( b) as [a ].
    exists a. now apply IH with (t := (g b)).
Qed.


Hint Resolve Aeq_ref Aeq_sym Aeq_tra : core.

Instance aeq_equiv :
  Equivalence Aeq.
Proof.
  constructor; eauto.
Qed.


Definition Ain s '(Asup A f) :=
   a, Aeq s (f a).

Definition ASubq s t :=
   u, Ain u s Ain u t.

Lemma Ain_Asup A f a :
  Ain (f a) (Asup A f).
Proof.
  simpl. exists a. now apply Aeq_ref.
Qed.


Lemma Ain_pi s t :
  Ain s t a : ( t), Aeq s ( t a).
Proof.
  destruct t as [A f]. intros [a H]. now exists a.
Qed.


Lemma pi_Ain (s : Acz) (a : s) :
  Ain ( s a) s.
Proof.
  destruct s as [A f]; simpl in *. now exists a.
Qed.


Lemma Ain_mor s s' t t' :
  Aeq s s' Aeq t t' Ain s t Ain s' t'.
Proof.
  intros .
  destruct t as [ ]. simpl in . destruct as [ ].
  destruct t' as [ ]. simpl. simpl in . destruct as [ _].
  destruct ( ) as [ ]. exists .
  rewrite . now rewrite .
Qed.


Instance Ain_proper :
  Proper (Aeq Aeq iff) Ain.
Proof.
  intros s s' t t' . split; intros H.
  - now apply (Ain_mor ).
  - apply Aeq_sym in . apply Aeq_sym in .
    now apply (Ain_mor ).
Qed.


Instance ASubq_proper :
  Proper (Aeq Aeq iff) ASubq.
Proof.
  intros s s' t t' . split; intros H.
  - intros u. rewrite , . apply H.
  - intros u. rewrite , . apply H.
Qed.



Definition AEmpty :=
  Asup False ( a match a with end).

Definition Aupair X Y :=
  Asup bool ( a if a then X else Y).

Definition Aunion '(Asup A f) :=
  Asup (sigT ( (a : A) ( (f a)))) ( p let (a, b) := p in (f a) b).

Definition Apower '(Asup A f) :=
  Asup (A Prop) ( P Asup (sig P) ( p let (a, _) := p in f a)).

Definition Asep (P : Acz Prop) '(Asup A f) :=
  Asup (sig ( a P (f a))) ( p let (a, _) := p in f a).

Definition Arepl (F : Acz Acz) '(Asup A f) :=
  Asup A ( a F (f a)).

Definition Asucc X :=
  Aunion (Aupair X (Aupair X X)).

Fixpoint Anumeral n :=
  match n with
  | 0 AEmpty
  | S n Asucc (Anumeral n)
  end.

Definition Aom :=
  Asup Anumeral.



Lemma Aeq_ext s t :
  ASubq s t ASubq t s Aeq s t.
Proof.
  destruct s as [A f], t as [B g].
  intros . simpl. split.
  - intros a. destruct ( (f a) (Ain_Asup f a)) as [b ]. now exists b.
  - intros b. destruct ( (g b) (Ain_Asup g b)) as [a ]. now exists a.
Qed.


Lemma Aeq_ASubq s t :
  Aeq s t ASubq s t.
Proof.
  destruct s as [A f], t as [B g]. intros [H _] z [a Z].
  destruct (H a) as [b I]. exists b. eauto.
Qed.



Lemma AEmptyAx s :
   Ain s AEmpty.
Proof.
  now intros [t H].
Qed.



Lemma AupairAx s t u :
  Ain u (Aupair s t) Aeq u s Aeq u t.
Proof.
  split; intros H.
  - destruct H as [[] H]; auto.
  - destruct H as [H|H]; [now exists true | now exists false].
Qed.


Lemma Aupair_mor s s' t t' u :
  Aeq s s' Aeq t t' Ain u (Aupair s t) Ain u (Aupair s' t').
Proof.
  intros H. apply AupairAx.
  rewrite , . now apply AupairAx in H.
Qed.


Instance Aupair_proper :
  Proper (Aeq Aeq Aeq) Aupair.
Proof.
  intros s s' t t' . apply Aeq_ext; intros z H.
  - now apply (Aupair_mor ).
  - symmetry in , . now apply (Aupair_mor ).
Qed.



Lemma AunionAx s u :
  Ain u (Aunion s) t, Ain t s Ain u t.
Proof.
  split; intros H; destruct s as [A f].
  - destruct H as [[a b] H]. exists (f a). split.
    + now exists a.
    + destruct (f a) as [C h]; simpl in *. now exists b.
  - destruct H as [[B g][[a ][b ]]].
    apply Aeq_ASubq in .
    specialize ( (g b) (Ain_Asup g b)).
    apply Ain_pi in as [c H].
    exists (existT _ a c). eauto.
Qed.


Lemma Aunion_mor s s' u :
  Aeq s s' Ain u (Aunion s) Ain u (Aunion s').
Proof.
  intros . apply AunionAx in as [t ].
  rewrite in . apply AunionAx. now exists t.
Qed.


Instance Aunion_proper :
  Proper (Aeq Aeq) Aunion.
Proof.
  intros s s' . apply Aeq_ext; intros z H.
  - now apply (Aunion_mor ).
  - symmetry in . now apply (Aunion_mor ).
Qed.



Lemma ApowerAx s t :
  Ain t (Apower s) ASubq t s.
Proof.
  split; intros H; destruct s as [A f].
  - destruct H as [P H].
    intros u Z. apply Aeq_ASubq in H.
    destruct (H u Z) as [[a PA] I]. now exists a.
  - exists ( a Ain (f a) t). apply Aeq_ext; intros z Z.
    + destruct t as [B g], Z as [b ].
      destruct (H (g b) (Ain_Asup g b)) as [a J].
      assert (: Ain (f a) (Asup B g)) by (exists b; auto).
      exists (exist _ a ). eauto.
    + destruct Z as [[a YA] % Aeq_sym].
      now apply (Ain_mor (t:=t)).
Qed.


Lemma Apower_mor s s' t :
  Aeq s s' Ain t (Apower s) Ain t (Apower s').
Proof.
  intros . apply ApowerAx.
  rewrite . now apply ApowerAx.
Qed.


Instance Apower_proper :
  Proper (Aeq Aeq) Apower.
Proof.
  intros s s' . apply Aeq_ext; intros z H.
  - now apply (Apower_mor ).
  - symmetry in . now apply (Apower_mor ).
Qed.



Definition cres X (R : X X Prop) (P : X Prop) :=
   x y, R x y P x P y.

Lemma AsepAx (P : Acz Prop) s t :
  cres Aeq P Ain t (Asep P s) Ain t s P t.
Proof.
  intros HP. split; intros H; destruct s as [A f].
  - destruct H as [[a PA]H].
    split; eauto. now exists a.
  - destruct H as [[a H]PY].
    assert (PA : P (f a)) by now apply (HP t).
    now exists (exist _ a PA).
Qed.


Lemma Asep_mor (P P' : Acz Prop) s s' t :
  cres Aeq P cres Aeq P' ( s, P s P' s)
   Aeq s s' Ain t (Asep P s) Ain t (Asep P' s').
Proof.
  intros . apply AsepAx; trivial.
  rewrite , . apply AsepAx; trivial.
Qed.


Lemma Asep_proper' (P P' : Acz Prop) s s' :
  cres Aeq P cres Aeq P' ( s, P s P' s)
   Aeq s s' Aeq (Asep P s) (Asep P' s').
Proof.
  intros . apply Aeq_ext; intros z Z.
  - apply (Asep_mor ); assumption.
  - apply (@Asep_mor P' P s' s); firstorder.
Qed.


Lemma Asep_proper (P : Acz Prop) s s' :
  cres Aeq P Aeq s s' Aeq (Asep P s) (Asep P s').
Proof.
  intros . apply (@Asep_proper' P P); firstorder.
Qed.



Definition fres X (R : X X Prop) (f : X X) :=
   x y, R x y R (f x) (f y).

Lemma AreplAx F s u :
  fres Aeq F Ain u (Arepl F s) t, Ain t s Aeq u (F t).
Proof.
  intros HF. split; intros H; destruct s as [A f].
  - destruct H as [a H]. exists (f a).
    split; trivial. apply Ain_Asup.
  - destruct H as [z[[a H] Z]].
    exists a. apply HF in H; try now exists a.
    now rewrite Z, H.
Qed.


Lemma Arepl_mor (F F' : Acz Acz) s s' u :
  fres Aeq F fres Aeq F' ( s, Aeq (F s) (F' s))
   Aeq s s' Ain u (Arepl F s) Ain u (Arepl F' s').
Proof.
  intros . apply AreplAx; trivial.
  apply AreplAx in as [y H]; trivial.
  exists y. now rewrite , .
Qed.


Lemma Arepl_proper' (F F' : Acz Acz) s s' :
  fres Aeq F fres Aeq F' ( s, Aeq (F s) (F' s))
   Aeq s s' Aeq (Arepl F s) (Arepl F' s').
Proof.
  intros . apply Aeq_ext; intros z Z.
  - apply (Arepl_mor ); assumption.
  - apply (@Arepl_mor F' F s' s); auto.
Qed.


Lemma Arepl_proper (F : Acz Acz) s s' :
 fres Aeq F Aeq s s' Aeq (Arepl F s) (Arepl F s').
Proof.
  intros . now apply Arepl_proper'.
Qed.



Instance Asucc_proper :
  Proper (Aeq Aeq) Asucc.
Proof.
  intros s s' . unfold Asucc. now rewrite .
Qed.


Definition Ainductive X :=
  Ain AEmpty X s, Ain s X Ain (Asucc s) X.

Lemma AomAx1 :
  Ainductive Aom.
Proof.
  split.
  - exists 0. apply Aeq_ref.
  - intros s [n H]. exists (S n). now rewrite H.
Qed.


Lemma AomAx2 X :
  Ainductive X ASubq Aom X.
Proof.
  intros H s [n ]. induction n; now apply H.
Qed.