(* The definitions and other results of age_by and age_to should be
moved here from msl/ageable.v.  Alternatively, this can be moved to
msl/ageable.v (or this file to msl/) eventually, but we keep it here
for now to reduce compilation time. *)

Require Import Coq.omega.Omega.
Require Import VST.msl.ageable.
Require Import VST.msl.predicates_hered.
Require Import VST.msl.sepalg.
Require Import VST.msl.age_sepalg.
Require Import VST.msl.sepalg_generators.

(* Apply [age1] n times (meaningful when [n <= level x] *)

Definition age1' {A} `{agA : ageable A} : A -> A :=
  fun x => match age1 x with Some y => y | None => x end.

Definition age_by n {A} `{agA : ageable A} : A -> A := Nat.iter n age1'.

Lemma level_age1' {A} `{agA : ageable A} x : level (age1' x) = level x - 1.
Proof.
(* Goal: forall _ : @app_pred A agA R x, @app_pred A agA R (@age1' A agA x) *)
  unfold age1'. destruct (age1 x) eqn:E.
  - apply age_level in E. omega.
  - apply age1_level0 in E. omega.
Qed.

Lemma level_age_by n {A} `{agA : ageable A} x : level (age_by n x) = level x - n.
Proof.
(* Goal: @eq (option A) (@composeOptN A f n x) (@composeOptN' A f n x) *)
  revert x; induction n; intros x; simpl.
  - omega.
  - simpl. rewrite level_age1'. rewrite IHn. omega.
Qed.

Lemma age_age_by n {A} `{agA : ageable A} (x y : A) : age x y -> age_by (S n) x = age_by n y.
Proof.
(* Goal: forall _ : ge k (@level A agA x), @eq A (@age_to k A agA x) x *)
  intros E.
(* Goal: @eq A (@age_by (S n) A agA x) (@age_by n A agA y) *)
  induction n.
  - simpl.
(* Goal: @eq A (@age1' A agA x) y *)
    unfold age1' in *.
(* Goal: @eq A (@age_by (Init.Nat.sub (@level A agA x) n) A agA x) y *)
    rewrite E. auto.
  - change (age1' (age_by (S n) x) = age_by (S n) y).
(* Goal: @eq A (@age1' A agA (@age_by (S n) A agA x)) (@age_by (S n) A agA y) *)
    rewrite IHn.
(* Goal: @eq A y y *)
    reflexivity.
Qed.

(* Age [x] to the level [k] (meaningul when [k <= level x] *)
Definition age_to k {A} `{agA : ageable A} (x : A) : A := age_by (level x - k) x.

Lemma level_age_to k {A} `{agA : ageable A} x : k <= level x -> level (age_to k x) = k.
Proof.
(* Goal: forall _ : lt k (@level A agA x), @ex A (fun y : A => and (@age A agA x y) (@eq A (@age_to k A agA x) (@age_to k A agA y))) *)
  intros L. unfold age_to.
(* Goal: @age A X x x *)
  rewrite level_age_by; omega.
Qed.

(* Proof techniques for age_to *)
Lemma age_to_lt k {A} `{agA : ageable A} (x : A) : k < level x -> exists y, age x y /\ age_to k x = age_to k y.
Proof.
(* Goal: forall _ : lt k (@level A agA x), @ex A (fun y : A => and (@age A agA x y) (@eq A (@age_to k A agA x) (@age_to k A agA y))) *)
  intros L.
(* Goal: @ex A (fun y : A => and (@age A agA x y) (@eq A (@age_to k A agA x) (@age_to k A agA y))) *)
  destruct (age1 x) as [y|] eqn:Ex; swap 1 2.
  - rewrite age1_level0 in Ex. omega.
  - exists y; split; auto.
(* Goal: @eq A (@age_to n A agA x) y *)
    unfold age_to.
(* Goal: @eq A (@age_by (Init.Nat.sub (@level A agA x) k) A agA x) (@age_by (Init.Nat.sub (@level A agA y) k) A agA y) *)
    pose proof age_level _ _ Ex as E.
    replace (level x - k) with (S (level y - k)) by omega.
    generalize (level y - k).
(* Goal: forall n : nat, @eq A (@age_by (S n) A agA x) (@age_by n A agA y) *)
    clear E L.
(* Goal: forall n : nat, @eq A (@age_by (S n) A agA x) (@age_by n A agA y) *)
    intros.
(* Goal: @eq A (@age_by (S n) A agA x) (@age_by n A agA y) *)
    apply age_age_by, Ex.
Qed.

Lemma age_to_ge k {A} `{agA : ageable A} (x : A) : k >= level x -> age_to k x = x.
Proof.
(* Goal: forall _ : ge k (@level A agA x), @eq A (@age_to k A agA x) x *)
  intros E. unfold age_to.
  replace (level x - k) with 0 by auto with *.
(* Goal: @eq A y y *)
  reflexivity.
Qed.

Lemma age_to_eq k {A} `{agA : ageable A} (x : A) : k = level x -> age_to k x = x.
Proof.
  intros ->; apply age_to_ge, le_refl.
Qed.

Lemma age_age_to n {A} `{agA : ageable A} x y : level x = S n -> age x y -> age_to n x = y.
Proof.
(* Goal: forall (_ : @eq nat (@level A agA x) (S n)) (_ : @age A agA x y), @eq A (@age_to n A agA x) y *)
  intros E Y.
(* Goal: @age A X x x *)
  assert (L : (n < level x)%nat) by omega.
  unfold age_to. rewrite E. replace (S n - n) with 1 by omega.
(* Goal: forall _ : @app_pred A agA R x, @app_pred A agA R (@age1' A agA x) *)
  simpl. unfold age1'. rewrite Y. reflexivity.
Qed.

Lemma age_by_ind {A} `{agA : ageable A} (P : A -> Prop) :
  (forall x y, age x y -> P x -> P y) ->
  forall x n, P x -> P (age_by n x).
Proof.
(* Goal: forall (_ : forall (x y : A) (_ : @age A agA x y) (_ : P y), P x) (x : A) (n : nat) (_ : P (@age_to n A agA x)), P x *)
  intros IH x n.
(* Goal: forall _ : P (@age_by n A agA x), P x *)
  unfold age_by.
(* Goal: forall _ : P (Nat.iter n A (@age1' A agA) x), P x *)
  induction n; intros Px.
  - auto.
  - simpl. unfold age1' at 1.
(* Goal: @eq (option A) (@Some A x) (@Some A x) *)
(* Goal: @eq (option A) match f x with | Some w' => @composeOptN A f n w' | None => @None A end match @composeOptN' A f n x with | Some y => f y | None => @None A end *)
    destruct (age1 (Nat.iter n age1' x)) as [y|] eqn:Ey; auto.
(* Goal: @eq (option A) (@Some A x) (@Some A x) *)
(* Goal: @eq (option A) match f x with | Some w' => @composeOptN A f n w' | None => @None A end match @composeOptN' A f n x with | Some y => f y | None => @None A end *)
    eapply IH; eauto.
Qed.

Lemma age_to_ind {A} `{agA : ageable A} (P : A -> Prop) :
  (forall x y, age x y -> P x -> P y) ->
  forall x n, P x -> P (age_to n x).
Proof.
(* Goal: forall (_ : forall (x y : A) (_ : @age A agA x y) (_ : P y), P x) (x : A) (n : nat) (_ : P (@age_to n A agA x)), P x *)
  intros IH x n.
(* Goal: forall _ : P x, P (@age_to n A agA x) *)
  apply age_by_ind, IH.
Qed.

Lemma age_to_ind_refined n {A} `{agA : ageable A} (P : A -> Prop) :
  (forall x y, age x y -> n <= level y -> P x -> P y) ->
  forall x, P x -> P (age_to n x).
Proof.
(* Goal: forall (_ : forall (x y : A) (_ : @age A agA x y) (_ : le n (@level A agA y)) (_ : P x), P y) (x : A) (_ : P x), P (@age_to n A agA x) *)
  intros IH x Px.
(* Goal: @age A X x x *)
  assert (dec : n >= level x \/ n <= level x) by omega.
(* Goal: P (@age_to n A agA x) *)
  destruct dec as [Ge|Le].
  - rewrite age_to_ge; auto.
  - eapply (age_to_ind (fun x => n <= level x -> P x)); auto.
    + intros x0 y H H0 H1.
(* Goal: @eq (option A) (@Some A x) (@Some A x) *)
(* Goal: @eq (option A) match f x with | Some w' => @composeOptN A f n w' | None => @None A end match @composeOptN' A f n x with | Some y => f y | None => @None A end *)
      eapply IH; eauto.
(* Goal: P x0 *)
      apply age_level in H.
(* Goal: P x0 *)
      apply H0.
(* Goal: @age A X x x *)
      omega.
(* Goal: @eq (option A) (@Some A x) (@Some A x) *)
(* Goal: @eq (option A) match f x with | Some w' => @composeOptN A f n w' | None => @None A end match @composeOptN' A f n x with | Some y => f y | None => @None A end *)
    + rewrite level_age_to; auto.
Qed.

Lemma iter_iter n m {A} f (x : A) : Nat.iter n f (Nat.iter m f x) = Nat.iter (n + m) f x.
Proof.
(* Goal: P (Nat.iter (S n) A (@age1' A agA) x) *)
  induction n; auto; simpl. rewrite IHn; auto.
Qed.

Lemma age_by_age_by n m  {A} `{agA : ageable A} (x : A) : age_by n (age_by m x) = age_by (n + m) x.
Proof.
(* Goal: @eq A (@age_by n A agA (@age_by m A agA x)) (@age_by (Init.Nat.add n m) A agA x) *)
  apply iter_iter.
Qed.

Lemma age_by_ind_opp {A} `{agA : ageable A} (P : A -> Prop) :
  (forall x y, age x y -> P y -> P x) ->
  forall x n, P (age_by n x) -> P x.
Proof.
(* Goal: forall (_ : forall (x y : A) (_ : @age A agA x y) (_ : P y), P x) (x : A) (n : nat) (_ : P (@age_to n A agA x)), P x *)
  intros IH x n.
(* Goal: forall _ : P (@age_by n A agA x), P x *)
  unfold age_by.
(* Goal: forall _ : P (Nat.iter n A (@age1' A agA) x), P x *)
  induction n; intros Px.
  - auto.
  - simpl in Px. unfold age1' at 1 in Px.
(* Goal: @eq (option A) (@Some A x) (@Some A x) *)
(* Goal: @eq (option A) match f x with | Some w' => @composeOptN A f n w' | None => @None A end match @composeOptN' A f n x with | Some y => f y | None => @None A end *)
    destruct (age1 (Nat.iter n age1' x)) as [y|] eqn:Ey; auto.
(* Goal: @eq (option A) (@Some A x) (@Some A x) *)
(* Goal: @eq (option A) match f x with | Some w' => @composeOptN A f n w' | None => @None A end match @composeOptN' A f n x with | Some y => f y | None => @None A end *)
    eapply IH in Ey; eauto.
Qed.

Lemma age_to_ind_opp {A} `{agA : ageable A} (P : A -> Prop) :
  (forall x y, age x y -> P y -> P x) ->
  forall x n, P (age_to n x) -> P x.
Proof.
(* Goal: forall (_ : forall (x y : A) (_ : @age A agA x y) (_ : P y), P x) (x : A) (n : nat) (_ : P (@age_to n A agA x)), P x *)
  intros IH x n.
(* Goal: forall _ : P (@age_to n A agA x), P x *)
  apply age_by_ind_opp, IH.
Qed.

Lemma rewrite_age_to {A} `{agA : ageable A} (P : A -> Prop) :
  (forall x y, age x y -> P x <-> P y) ->
  forall x n, P x <-> P (age_to n x).
Proof.
(* Goal: forall (_ : forall (x y : A) (_ : @age A agA x y), iff (P x) (P y)) (x : A) (n : nat), iff (P x) (P (@age_to n A agA x)) *)
  intros IH x n; split.
  - apply age_to_ind. intros; rewrite <-IH; eauto.
  - apply age_to_ind_opp. intros; rewrite IH; eauto.
Qed.

Lemma level_age_to_le k {A} `{agA : ageable A} x : level (age_to k x) <= level x.
Proof.
(* Goal: @eq (option A) (@Some A x) (@Some A x) *)
(* Goal: @eq (option A) match f x with | Some w' => @composeOptN A f n w' | None => @None A end match @composeOptN' A f n x with | Some y => f y | None => @None A end *)
  destruct (le_lt_dec k (level x)) as [l|l]. rewrite level_age_to; auto.
(* Goal: @age A X x x *)
  rewrite age_to_ge; omega.
Qed.

Lemma level_age_to_le' k {A} `{agA : ageable A} x : level (age_to k x) <= k.
Proof.
(* Goal: @eq (option A) (@Some A x) (@Some A x) *)
(* Goal: @eq (option A) match f x with | Some w' => @composeOptN A f n w' | None => @None A end match @composeOptN' A f n x with | Some y => f y | None => @None A end *)
  destruct (le_lt_dec k (level x)) as [l|l]. rewrite level_age_to; auto.
(* Goal: @age A X x x *)
  rewrite age_to_ge; omega.
Qed.

Lemma age_by_necR {A} `{agA : ageable A} n x : necR x (age_by n x).
Proof.
(* Goal: @necR A agA x (@age_by n A agA x) *)
  generalize (necR_refl x).
(* Goal: forall _ : @necR A agA x x, @necR A agA x (@age_by n A agA x) *)
  generalize x at 1 3; intros u.
(* Goal: forall _ : @necR A agA u x, @necR A agA u (@age_by n A agA x) *)
  apply age_by_ind; clear x.
(* Goal: forall (x y : A) (_ : @age A agA x y) (_ : @necR A agA u x), @necR A agA u y *)
  intros x y a N.
(* Goal: @eq (option A) (@Some A x) (@Some A x) *)
(* Goal: @eq (option A) match f x with | Some w' => @composeOptN A f n w' | None => @None A end match @composeOptN' A f n x with | Some y => f y | None => @None A end *)
  constructor 3 with x; auto.
(* Goal: @eq (option A) (@Some A x) (@Some A x) *)
(* Goal: @eq (option A) match f x with | Some w' => @composeOptN A f n w' | None => @None A end match @composeOptN' A f n x with | Some y => f y | None => @None A end *)
  constructor; auto.
Qed.

Lemma age_to_necR {A} `{agA : ageable A} n x : necR x (age_to n x).
Proof.
(* Goal: @necR A agA x (@age_by (Init.Nat.sub (@level A agA x) (@level A agA x')) A agA x) *)
  apply age_by_necR.
Qed.

Lemma necR_age_by {A} `{agA : ageable A} x x' : necR x x' -> x' = age_by (level x - level x') x.
Proof.
  intros N; induction N.
  - rewrite (age_level _ _ H).
    replace (S _ - _) with 1. 2:omega.
(* Goal: forall _ : @app_pred A agA R x, @app_pred A agA R (@age1' A agA x) *)
    simpl. unfold age1'. rewrite H; auto.
  - replace (_ - _) with 0. 2:omega. reflexivity.
  - rewrite IHN2, IHN1.
    rewrite age_by_age_by.
    repeat rewrite level_age_by.
    f_equal.
    apply necR_level in N1.
    apply necR_level in N2.
    replace (_ x - (_ x - _ y)) with (level y) by omega.
    replace (_ y - _ z + (_ x - _ y)) with (level x - level z) by omega.
(* Goal: @age A X x x *)
    omega.
Qed.

Lemma necR_age_to {A} `{agA : ageable A} x x' : necR x x' -> x' = age_to (level x') x.
Proof.
(* Goal: forall _ : @necR A agA x x', @eq A x' (@age_by (Init.Nat.sub (@level A agA x) (@level A agA x')) A agA x) *)
(* Goal: forall _ : @eq A x' (@age_by (Init.Nat.sub (@level A agA x) (@level A agA x')) A agA x), @necR A agA x x' *)
  apply necR_age_by.
Qed.

Lemma necR_age_by_iff {A} `{agA : ageable A} x x' : necR x x' <-> x' = age_by (level x - level x') x.
Proof.
  split. apply necR_age_by. intros ->. apply age_by_necR.
Qed.

Lemma necR_age_to_iff {A} `{agA : ageable A} x x' : necR x x' <-> x' = age_to (level x') x.
Proof.
(* Goal: iff (@necR A agA x x') (@eq A x' (@age_to (@level A agA x') A agA x)) *)
  apply necR_age_by_iff.
Qed.

Lemma age_to_pred {A} `{agA : ageable A} (P : pred A) x n :
  app_pred P x ->
  app_pred P (age_to n x).
Proof.
(* Goal: forall _ : @app_pred A agA P x, @app_pred A agA P (@age_to n A agA x) *)
  apply age_to_ind. clear x n.
(* Goal: forall (x y : A) (_ : @age A agA x y) (_ : @app_pred A agA P x), @app_pred A agA P y *)
  destruct P as [x h]. apply h.
Qed.

Lemma age_by_pred {A} `{agA : ageable A} (P : pred A) x n :
  app_pred P x ->
  app_pred P (age_by n x).
Proof.
(* Goal: forall (x y : A) (_ : @age A agA x y) (_ : @app_pred A agA P x), @app_pred A agA P y *)
  apply age_by_ind. clear x n.
(* Goal: forall (x y : A) (_ : @age A agA x y) (_ : @app_pred A agA P x), @app_pred A agA P y *)
  destruct P as [x h]. apply h.
Qed.

Lemma pred_age1' {A} `{agA : ageable A} (R : pred A) x : app_pred R x -> app_pred R (age1' x).
Proof.
(* Goal: forall _ : @app_pred A agA R x, @app_pred A agA R (@age1' A agA x) *)
  unfold age1'. destruct (age1 x) as [phi' | ] eqn:Ephi'; auto.
(* Goal: forall _ : @app_pred A agA (@exist (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A agA) p) R h) x, @app_pred A agA (@exist (forall _ : A, Prop) (fun p : forall _ : A, Prop => @hereditary A (@age A agA) p) R h) phi' *)
  destruct R as [R h]. apply h. apply Ephi'.
Qed.

Lemma age_by_age_by_pred {A} `{agA : ageable A} (P : pred A) x n1 n2 :
  le n1 n2 ->
  app_pred P (age_by n1 x) ->
  app_pred P (age_by n2 x).
Proof.
  intros l. replace n2 with ((n2 - n1) + n1) by auto with *.
  rewrite <-age_by_age_by.
(* Goal: forall _ : @app_pred A agA P (@age_by n1 A agA x), @app_pred A agA P (@age_by (Init.Nat.sub n2 n1) A agA (@age_by n1 A agA x)) *)
  apply age_by_pred.
Qed.

Fixpoint composeOptN' {A} (f : A -> option A) n x :=
  match n with
  | 0 => Some x
  | S n =>
    match composeOptN' f n x with
    | Some y => f y
    | None => None
    end
  end.

Lemma composeOptN_assoc_aux_None {A} (f : A -> option A) n x :
  f x = None ->
  match composeOptN f n x with
  | Some x => f x
  | None => None
  end = None.
Proof.
(* Goal: @eq (option A) (@Some A x) (@Some A x) *)
(* Goal: @eq (option A) match f x with | Some w' => @composeOptN A f n w' | None => @None A end match @composeOptN' A f n x with | Some y => f y | None => @None A end *)
  revert x; induction n; intros x E; simpl; auto.
(* Goal: @eq (option A) match match f x with | Some w' => @composeOptN A f n w' | None => @None A end with | Some x => f x | None => @None A end (@None A) *)
  destruct (f x); congruence.
Qed.

Lemma composeOptN_assoc_aux_Some {A} (f : A -> option A) n x y :
  f x = Some y ->
  match composeOptN f n x with
  | Some x => f x
  | None => None
  end = composeOptN f n y.
Proof.
(* Goal: P (Nat.iter (S n) A (@age1' A agA) x) *)
  revert x y; induction n; intros x y Ey; simpl. auto.
(* Goal: @eq (option A) match match f x with | Some w' => @composeOptN A f n w' | None => @None A end with | Some x => f x | None => @None A end match f y with | Some w' => @composeOptN A f n w' | None => @None A end *)
  rewrite Ey.
(* Goal: @eq (option A) match @composeOptN A f n y with | Some x => f x | None => @None A end match f y with | Some w' => @composeOptN A f n w' | None => @None A end *)
  destruct (f y) as [z|] eqn:Ez.
  - eauto.
  - apply composeOptN_assoc_aux_None, Ez.
Qed.

Lemma composeOptN_assoc {A} (f : A -> option A) n x :
  composeOptN f n x = composeOptN' f n x.
Proof.
(* Goal: @eq (option A) (@composeOptN A f n x) (@composeOptN' A f n x) *)
  revert x; induction n; intros x; simpl. auto.
  destruct (f x) as [y|] eqn:Ey; rewrite <-IHn.
  - erewrite composeOptN_assoc_aux_Some; eauto.
  - rewrite composeOptN_assoc_aux_None; eauto.
Qed.

Lemma age_by_ageN {A} `{agA : ageable A} n (x : A) :
  n <= level x ->
  ageN n x = Some (age_by n x).
Proof.
(* Goal: @eq A y y *)
  revert x; induction n; intros x l. reflexivity.
  unfold ageN.
  rewrite composeOptN_assoc; simpl; rewrite <-composeOptN_assoc.
  change (composeOptN age1 n x) with (ageN n x).
(* Goal: @age A X x x *)
  rewrite IHn. 2:omega.
(* Goal: @eq A (@age1' A agA x) y *)
  unfold age1' in *.
(* Goal: @eq (option A) (@Some A x) (@Some A x) *)
(* Goal: @eq (option A) match f x with | Some w' => @composeOptN A f n w' | None => @None A end match @composeOptN' A f n x with | Some y => f y | None => @None A end *)
  destruct (age1 (age_by n x)) as [y|] eqn:Ey. auto.
  exfalso. rewrite age1_level0 in Ey.
(* Goal: @age A X x x *)
  rewrite level_age_by in Ey. omega.
Qed.

Lemma age_to_ageN {A} `{agA : ageable A} n (x : A) :
  ageN (level x - n) x = Some (age_to n x).
Proof.
(* Goal: @eq (option A) (@ageN A agA (Init.Nat.sub (@level A agA x) n) x) (@Some A (@age_to n A agA x)) *)
  apply age_by_ageN. auto with *.
Qed.

Lemma age_by_1 {A} {_ : ageable A} x : 0 < level x -> age x (age_by 1 x).
Proof.
(* Goal: forall _ : lt O (@level A X x), @age A X x (@age_by (S O) A X x) *)
  intros l.
(* Goal: P (Nat.iter (S n) A (@age1' A agA) x) *)
  unfold age_by, age1'; simpl.
(* Goal: @eq (option A) (@Some A x) (@Some A x) *)
(* Goal: @eq (option A) match f x with | Some w' => @composeOptN A f n w' | None => @None A end match @composeOptN' A f n x with | Some y => f y | None => @None A end *)
  destruct (age1 x) eqn:E; eauto.
(* Goal: @age A X x x *)
  apply age1_level0 in E.
(* Goal: @age A X x x *)
  omega.
Qed.

Lemma age_to_1 {A} {_ : ageable A} n x : level x = S n -> age x (age_to n x).
Proof.
(* Goal: @eq A (@age_by (Init.Nat.sub (@level A agA x) n) A agA x) y *)
  unfold age_to; intros E; rewrite E.
  replace (S n - n) with 1 by auto with *.
(* Goal: lt O (@level A X x) *)
  apply age_by_1. auto with *.
Qed.

Lemma age_to_identy {A} `{asaA: Age_alg A}: forall k phi,
    identity phi -> identity (age_to k phi).
Proof.
  intros k phi. unfold age_to. generalize (level phi - k); intros n; revert phi.
(* Goal: forall _ : @app_pred A agA R x, @app_pred A agA R (@age1' A agA x) *)
  induction n; intros phi id; simpl; auto. unfold age1'.
(* Goal: @eq (option A) (@Some A x) (@Some A x) *)
(* Goal: @eq (option A) match f x with | Some w' => @composeOptN A f n w' | None => @None A end match @composeOptN' A f n x with | Some y => f y | None => @None A end *)
  destruct (age1 (age_by n phi)) eqn:E; auto.
(* Goal: @eq (option A) (@Some A x) (@Some A x) *)
(* Goal: @eq (option A) match f x with | Some w' => @composeOptN A f n w' | None => @None A end match @composeOptN' A f n x with | Some y => f y | None => @None A end *)
  eapply age_identity. apply E. auto.
Qed.

Lemma age_to_join_eq {A}  {JA: Join A}{PA: Perm_alg A}{agA: ageable A}{AgeA: Age_alg A} :
  forall k x1 x2 x3,
    join x1 x2 x3 ->
    k <= level x3 ->
    join (age_to k x1) (age_to k x2) (age_to k x3).
Proof.
(* Goal: forall (k : nat) (x1 x2 x3 : A) (_ : @join A JA x1 x2 x3) (_ : le k (@level A agA x3)), @join A JA (@age_to k A agA x1) (@age_to k A agA x2) (@age_to k A agA x3) *)
  intros k x1 x2 x3 J.
(* Goal: forall _ : le k (@level A agA x3), @join A JA (@age_to k A agA x1) (@age_to k A agA x2) (@age_to k A agA x3) *)
  remember (level x3) as l3 eqn:e3; symmetry in e3.
(* Goal: forall _ : le k l3, @join A JA (@age_to k A agA x1) (@age_to k A agA x2) (@age_to k A agA x3) *)
  pose proof join_level _ _ _ J as [e1 e2]; rewrite e3 in e1, e2.
(* Goal: forall _ : le k l3, @join A JA (@age_to k A agA x1) (@age_to k A agA x2) (@age_to k A agA x3) *)
  revert l3 x1 x2 x3 e1 e2 e3 J.
(* Goal: forall (l3 : nat) (x1 x2 x3 : A) (_ : @eq nat (@level A agA x1) l3) (_ : @eq nat (@level A agA x2) l3) (_ : @eq nat (@level A agA x3) l3) (_ : @join A JA x1 x2 x3) (_ : le k l3), @join A JA (@age_to k A agA x1) (@age_to k A agA x2) (@age_to k A agA x3) *)
  intros n; induction n as [ n IHn ] using strong_nat_ind. intros x1 x2 x3 e1 e2 e3 J L.
  destruct (le_lt_eq_dec _ _ L) as [Lt | ->]; swap 1 2.
(* Goal: @join A JA (@age_to n A agA x1) (@age_to n A agA x2) (@age_to n A agA x3) *)
(* Goal: @join A JA (@age_to k A agA x1) (@age_to k A agA x2) (@age_to k A agA x3) *)
  now do 3 (rewrite age_to_eq at 1; auto).
(* Goal: lt O (@level A X x) *)
  assert (l1 : k < level x1) by auto with *.
(* Goal: lt O (@level A X x) *)
  assert (l2 : k < level x2) by auto with *.
(* Goal: lt O (@level A X x) *)
  assert (l3 : k < level x3) by auto with *.
  destruct (age_to_lt _ x1 l1) as [x1' [E1 ->]].
  destruct (age_to_lt _ x2 l2) as [x2' [E2 ->]].
  destruct (age_to_lt _ x3 l3) as [x3' [E3 ->]].
(* Goal: @join A JA (@age_to k A agA x1') (@age_to k A agA x2') (@age_to k A agA x3') *)
  pose proof @age1_join_eq A _ _ _ _ _ _ _ J _ E1 _ E2 _ E3.
(* Goal: @join A JA (@age_to k A agA x1') (@age_to k A agA x2') (@age_to k A agA x3') *)
  pose proof @af_level2 A level age1 (@age_facts _ agA) _ _ E1.
(* Goal: @join A JA (@age_to k A agA x1') (@age_to k A agA x2') (@age_to k A agA x3') *)
  pose proof @af_level2 A level age1 (@age_facts _ agA) _ _ E2.
(* Goal: @join A JA (@age_to k A agA x1') (@age_to k A agA x2') (@age_to k A agA x3') *)
  pose proof @af_level2 A level age1 (@age_facts _ agA) _ _ E3.
(* Goal: @eq (option A) (@Some A x) (@Some A x) *)
(* Goal: @eq (option A) match f x with | Some w' => @composeOptN A f n w' | None => @None A end match @composeOptN' A f n x with | Some y => f y | None => @None A end *)
  apply IHn with (level x1'); omega || auto.
Qed.
