(* File: Lt_Ks.v  (last edited on 27/10/2000) (c) Klaus Weich  *)

Require Export Le.
Require Export Lt.
Require Export Le_Ks.


Fixpoint count_undecs (n : nested_imps) : nat :=
  match n with
  | nil => 0
  | Undecorated _ :: n => S (count_undecs n)
  | Decorated _ _ :: n => count_undecs n
  end.


Inductive Lt_Ks (ni1 : nested_imps) (dni1 : decorated_nested_imps)
(ni2 : nested_imps) (dni2 : decorated_nested_imps) : Set :=
  | lt_ks_count_undecs :
      le_ni (rev_app dni1 ni1) (rev_app dni2 ni2) ->
      count_undecs ni1 < count_undecs ni2 -> Lt_Ks ni1 dni1 ni2 dni2
  | lt_ks_length :
      le_ni (rev_app dni1 ni1) (rev_app dni2 ni2) ->
      length ni1 < length ni2 -> Lt_Ks ni1 dni1 ni2 dni2.


Lemma le_ni_le_count_undecs :
 forall ni1 ni2 : nested_imps,
 le_ni ni1 ni2 -> count_undecs ni1 <= count_undecs ni2.
(* Goal: forall (ni1 ni2 : nested_imps) (_ : le_ni ni1 ni2), le (count_undecs ni1) (count_undecs ni2) *)
intros ni1 ni2 le12.
(* Goal: le (count_undecs ni1) (count_undecs ni2) *)
elim le12; clear le12 ni1 ni2.
(* Goal: @eq nat (@length nested_imp (rev_app dni NNil)) (@length nested_imp (rev_app dni NNil)) *)
(* Goal: le_ni (@app nested_imp (rev_app dni NNil) ni) (@app nested_imp (rev_app dni NNil) ni) *)
(* Goal: lt (count_undecs ni1) (count_undecs (@cons nested_imp (Undecorated x) ni)) *)
trivial.
(* Goal: forall (x : nimp) (ni1 ni2 : nested_imps) (_ : le_ni ni1 ni2) (_ : le (count_undecs ni1) (count_undecs ni2)), le (count_undecs (@cons nested_imp (Undecorated x) ni1)) (count_undecs (@cons nested_imp (Undecorated x) ni2)) *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : le_ni ni1 ni2) (_ : le (count_undecs ni1) (count_undecs ni2)), le (count_undecs (@cons nested_imp (Decorated x k) ni1)) (count_undecs (@cons nested_imp (Undecorated x) ni2)) *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : le_ni ni1 ni2) (_ : le (count_undecs ni1) (count_undecs ni2)), le (count_undecs (@cons nested_imp (Decorated x k) ni1)) (count_undecs (@cons nested_imp (Decorated x k) ni2)) *)
intros x ni1 ni2 le ih; simpl in |- *.
(* Goal: Peano.le (S (count_undecs ni1)) (S (count_undecs ni2)) *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : le_ni ni1 ni2) (_ : le (count_undecs ni1) (count_undecs ni2)), le (count_undecs (@cons nested_imp (Decorated x k) ni1)) (count_undecs (@cons nested_imp (Undecorated x) ni2)) *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : le_ni ni1 ni2) (_ : le (count_undecs ni1) (count_undecs ni2)), le (count_undecs (@cons nested_imp (Decorated x k) ni1)) (count_undecs (@cons nested_imp (Decorated x k) ni2)) *)
apply le_n_S; assumption.
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : le_ni ni1 ni2) (_ : le (count_undecs ni1) (count_undecs ni2)), le (count_undecs (@cons nested_imp (Decorated x k) ni1)) (count_undecs (@cons nested_imp (Decorated x k) ni2)) *)
intros x k ni1 ni2 le ih; simpl in |- *. 
(* Goal: Peano.le (count_undecs ni1) (S (count_undecs ni2)) *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : le_ni ni1 ni2) (_ : le (count_undecs ni1) (count_undecs ni2)), le (count_undecs (@cons nested_imp (Decorated x k) ni1)) (count_undecs (@cons nested_imp (Decorated x k) ni2)) *)
apply le_trans with (count_undecs ni2).
(* Goal: lt (@length nested_imp ni1) (@length nested_imp ni) *)
(* Goal: le (@length nested_imp ni) m *)
assumption.
(* Goal: Peano.le (count_undecs ni2) (S (count_undecs ni2)) *)
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : le_ni ni1 ni2) (_ : le (count_undecs ni1) (count_undecs ni2)), le (count_undecs (@cons nested_imp (Decorated x k) ni1)) (count_undecs (@cons nested_imp (Decorated x k) ni2)) *)
apply le_n_Sn.
(* Goal: forall (x : nimp) (k : kripke_tree) (ni1 ni2 : nested_imps) (_ : le_ni ni1 ni2) (_ : le (count_undecs ni1) (count_undecs ni2)), le (count_undecs (@cons nested_imp (Decorated x k) ni1)) (count_undecs (@cons nested_imp (Decorated x k) ni2)) *)
intros x k ni1 ni2 le ih; simpl in |- *. 
(* Goal: lt (@length nested_imp ni1) (@length nested_imp ni) *)
(* Goal: le (@length nested_imp ni) m *)
assumption.
Qed.


Lemma count_undecs_rev_app :
 forall (dni : decorated_nested_imps) (ni : nested_imps),
 count_undecs (rev_app dni ni) = count_undecs ni.
(* Goal: forall (dni : decorated_nested_imps) (ni : nested_imps), @eq nat (count_undecs (rev_app dni ni)) (count_undecs ni) *)
intros dni; elim dni; clear dni.
(* Goal: @eq nat (@length nested_imp (rev_app dni NNil)) (@length nested_imp (rev_app dni NNil)) *)
(* Goal: le_ni (@app nested_imp (rev_app dni NNil) ni) (@app nested_imp (rev_app dni NNil) ni) *)
(* Goal: lt (count_undecs ni1) (count_undecs (@cons nested_imp (Undecorated x) ni)) *)
intros; trivial.
(* Goal: forall (a : decorated_nested_imp) (l : list decorated_nested_imp) (_ : forall ni : nested_imps, @eq nat (count_undecs (rev_app l ni)) (count_undecs ni)) (ni : nested_imps), @eq nat (count_undecs (rev_app (@cons decorated_nested_imp a l) ni)) (count_undecs ni) *)
intros x; case x; clear x.
(* Goal: forall (n : nimp) (k : kripke_tree) (l : list decorated_nested_imp) (_ : forall ni : nested_imps, @eq nat (count_undecs (rev_app l ni)) (count_undecs ni)) (ni : nested_imps), @eq nat (count_undecs (rev_app (@cons decorated_nested_imp (@pair nimp kripke_tree n k) l) ni)) (count_undecs ni) *)
intros x k dni ih ni.
(* Goal: le_ni (rev_app (@cons (prod nimp kripke_tree) (@pair nimp kripke_tree x k) dni) ni) (rev_app dni (@cons nested_imp (Undecorated x) ni)) *)
(* Goal: lt (count_undecs ni1) (count_undecs (@cons nested_imp (Undecorated x) ni)) *)
simpl in |- *.
(* Goal: @eq nat (count_undecs (rev_app dni (@cons nested_imp (Decorated x k) ni))) (count_undecs ni) *)
apply (ih (Decorated x k :: ni)).
Qed.


Lemma le_ks_le_count_undecs :
 forall (ni1 : nested_imps) (dni1 : decorated_nested_imps)
   (ni2 : nested_imps) (dni2 : decorated_nested_imps),
 le_ni (rev_app dni1 ni1) (rev_app dni2 ni2) ->
 count_undecs ni1 <= count_undecs ni2.
(* Goal: forall (ni1 : nested_imps) (dni1 : decorated_nested_imps) (ni2 : nested_imps) (dni2 : decorated_nested_imps) (_ : le_ni (rev_app dni1 ni1) (rev_app dni2 ni2)), le (count_undecs ni1) (count_undecs ni2) *)
intros ni1 dni1 ni2 dni2 le12.
generalize (le_ni_le_count_undecs (rev_app dni1 ni1) (rev_app dni2 ni2) le12);
 clear le12.
(* Goal: forall _ : le (count_undecs (rev_app dni1 ni1)) (count_undecs (rev_app dni2 ni2)), le (count_undecs ni1) (count_undecs ni2) *)
 rewrite (count_undecs_rev_app dni1 ni1).
(* Goal: forall _ : le (count_undecs ni1) (count_undecs (rev_app dni2 ni2)), le (count_undecs ni1) (count_undecs ni2) *)
 rewrite (count_undecs_rev_app dni2 ni2).
(* Goal: @eq nat (@length nested_imp (rev_app dni NNil)) (@length nested_imp (rev_app dni NNil)) *)
(* Goal: le_ni (@app nested_imp (rev_app dni NNil) ni) (@app nested_imp (rev_app dni NNil) ni) *)
(* Goal: lt (count_undecs ni1) (count_undecs (@cons nested_imp (Undecorated x) ni)) *)
trivial.
Qed.



Lemma My_Lt_Ks_rec :
 forall P : nested_imps -> Set,
 (forall (ni2 : nested_imps) (dni2 : decorated_nested_imps),
  (forall (ni1 : nested_imps) (dni1 : decorated_nested_imps),
   Lt_Ks ni1 dni1 ni2 dni2 -> P (rev_app dni1 ni1)) -> 
  P (rev_app dni2 ni2)) -> forall ni : nested_imps, P ni.
(* Goal: forall (P : forall _ : nested_imps, Set) (_ : forall (ni2 : nested_imps) (dni2 : decorated_nested_imps) (_ : forall (ni1 : nested_imps) (dni1 : decorated_nested_imps) (_ : Lt_Ks ni1 dni1 ni2 dni2), P (rev_app dni1 ni1)), P (rev_app dni2 ni2)) (ni : nested_imps), P ni *)
intros P step.
cut
 (forall (n m : nat) (ni : nested_imps) (dni : decorated_nested_imps),
  count_undecs ni < n -> length ni < m -> P (rev_app dni ni)).
(* Goal: forall (_ : forall (n m : nat) (ni : nested_imps) (dni : decorated_nested_imps) (_ : lt (count_undecs ni) n) (_ : lt (@length nested_imp ni) m), P (rev_app dni ni)) (ni : nested_imps), P ni *)
(* Goal: forall (n m : nat) (ni : nested_imps) (dni : decorated_nested_imps) (_ : lt (count_undecs ni) n) (_ : lt (@length nested_imp ni) m), P (rev_app dni ni) *)
intros claim ni.
apply
 claim
  with
    (n := S (count_undecs ni))
    (m := S (length ni))
    (ni := ni)
    (dni := DNI_NIL); clear claim.
(* Goal: lt (@length nested_imp ni1) (S (@length nested_imp ni1)) *)
(* Goal: P (rev_app dni1 ni1) *)
apply lt_n_Sn.
(* Goal: lt (@length nested_imp ni1) (S (@length nested_imp ni1)) *)
(* Goal: P (rev_app dni1 ni1) *)
apply lt_n_Sn.
(* Goal: forall (n m : nat) (ni : nested_imps) (dni : decorated_nested_imps) (_ : lt (count_undecs ni) n) (_ : lt (@length nested_imp ni) m), P (rev_app dni ni) *)
intros n; elim n; clear n.
(* Goal: forall (m : nat) (ni : nested_imps) (dni : decorated_nested_imps) (_ : lt (count_undecs ni) O) (_ : lt (@length nested_imp ni) m), P (rev_app dni ni) *)
(* Goal: forall (n : nat) (_ : forall (m : nat) (ni : nested_imps) (dni : decorated_nested_imps) (_ : lt (count_undecs ni) n) (_ : lt (@length nested_imp ni) m), P (rev_app dni ni)) (m : nat) (ni : nested_imps) (dni : decorated_nested_imps) (_ : lt (count_undecs ni) (S n)) (_ : lt (@length nested_imp ni) m), P (rev_app dni ni) *)
intros m ni dni lt_nonref lt_length.
(* Goal: P (rev_app dni ni) *)
(* Goal: forall (n0 : nat) (_ : forall (ni : nested_imps) (dni : decorated_nested_imps) (_ : lt (count_undecs ni) (S n)) (_ : lt (@length nested_imp ni) n0), P (rev_app dni ni)) (ni : nested_imps) (dni : decorated_nested_imps) (_ : lt (count_undecs ni) (S n)) (_ : lt (@length nested_imp ni) (S n0)), P (rev_app dni ni) *)
elimtype False.
(* Goal: False *)
(* Goal: forall (n : nat) (_ : forall (m : nat) (ni : nested_imps) (dni : decorated_nested_imps) (_ : lt (count_undecs ni) n) (_ : lt (@length nested_imp ni) m), P (rev_app dni ni)) (m : nat) (ni : nested_imps) (dni : decorated_nested_imps) (_ : lt (count_undecs ni) (S n)) (_ : lt (@length nested_imp ni) m), P (rev_app dni ni) *)
inversion_clear lt_nonref.
(* Goal: forall (n : nat) (_ : forall (m : nat) (ni : nested_imps) (dni : decorated_nested_imps) (_ : lt (count_undecs ni) n) (_ : lt (@length nested_imp ni) m), P (rev_app dni ni)) (m : nat) (ni : nested_imps) (dni : decorated_nested_imps) (_ : lt (count_undecs ni) (S n)) (_ : lt (@length nested_imp ni) m), P (rev_app dni ni) *)
intros n ih m.
(* Goal: forall (ni : nested_imps) (dni : decorated_nested_imps) (_ : lt (count_undecs ni) (S n)) (_ : lt (@length nested_imp ni) m), P (rev_app dni ni) *)
elim m; clear m.
(* Goal: forall (ni : nested_imps) (dni : decorated_nested_imps) (_ : lt (count_undecs ni) (S n)) (_ : lt (@length nested_imp ni) O), P (rev_app dni ni) *)
(* Goal: forall (n0 : nat) (_ : forall (ni : nested_imps) (dni : decorated_nested_imps) (_ : lt (count_undecs ni) (S n)) (_ : lt (@length nested_imp ni) n0), P (rev_app dni ni)) (ni : nested_imps) (dni : decorated_nested_imps) (_ : lt (count_undecs ni) (S n)) (_ : lt (@length nested_imp ni) (S n0)), P (rev_app dni ni) *)
intros ni dni lt_nonref lt_length.
(* Goal: P (rev_app dni ni) *)
(* Goal: forall (n0 : nat) (_ : forall (ni : nested_imps) (dni : decorated_nested_imps) (_ : lt (count_undecs ni) (S n)) (_ : lt (@length nested_imp ni) n0), P (rev_app dni ni)) (ni : nested_imps) (dni : decorated_nested_imps) (_ : lt (count_undecs ni) (S n)) (_ : lt (@length nested_imp ni) (S n0)), P (rev_app dni ni) *)
elimtype False.
(* Goal: False *)
(* Goal: forall (n0 : nat) (_ : forall (ni : nested_imps) (dni : decorated_nested_imps) (_ : lt (count_undecs ni) (S n)) (_ : lt (@length nested_imp ni) n0), P (rev_app dni ni)) (ni : nested_imps) (dni : decorated_nested_imps) (_ : lt (count_undecs ni) (S n)) (_ : lt (@length nested_imp ni) (S n0)), P (rev_app dni ni) *)
inversion_clear lt_length.
(* Goal: forall (n0 : nat) (_ : forall (ni : nested_imps) (dni : decorated_nested_imps) (_ : lt (count_undecs ni) (S n)) (_ : lt (@length nested_imp ni) n0), P (rev_app dni ni)) (ni : nested_imps) (dni : decorated_nested_imps) (_ : lt (count_undecs ni) (S n)) (_ : lt (@length nested_imp ni) (S n0)), P (rev_app dni ni) *)
intros m sih ni dni lt_nonref lt_length.
(* Goal: P (rev_app dni ni) *)
apply step; clear step.
(* Goal: forall (ni1 : nested_imps) (dni1 : decorated_nested_imps) (_ : Lt_Ks ni1 dni1 ni dni), P (rev_app dni1 ni1) *)
intros ni1 dni1 lt_ks.
(* Goal: P (rev_app dni1 ni1) *)
inversion_clear lt_ks.
(* Goal: P (rev_app dni1 ni1) *)
(* Goal: P (rev_app dni1 ni1) *)
apply ih with (S (length ni1)); clear ih.
(* Goal: lt (count_undecs ni1) n *)
(* Goal: lt (@length nested_imp ni1) (S (@length nested_imp ni1)) *)
(* Goal: P (rev_app dni1 ni1) *)
apply lt_S_n.
(* Goal: lt (@length nested_imp ni1) (@length nested_imp ni) *)
(* Goal: le (@length nested_imp ni) m *)
apply le_lt_trans with (count_undecs ni); assumption.
(* Goal: lt (@length nested_imp ni1) (S (@length nested_imp ni1)) *)
(* Goal: P (rev_app dni1 ni1) *)
apply lt_n_Sn.
(* Goal: P (rev_app dni1 ni1) *)
apply sih.
(* Goal: lt (count_undecs ni1) (count_undecs (@cons nested_imp (Undecorated x) ni)) *)
apply le_lt_trans with (count_undecs ni).
(* Goal: lt (@length nested_imp ni1) (@length nested_imp ni) *)
(* Goal: le (@length nested_imp ni) m *)
apply le_ks_le_count_undecs with dni1 dni; assumption.
(* Goal: lt (@length nested_imp ni1) (@length nested_imp ni) *)
(* Goal: le (@length nested_imp ni) m *)
assumption.
(* Goal: lt (@length nested_imp ni1) m *)
apply lt_le_trans with (length ni).
(* Goal: lt (@length nested_imp ni1) (@length nested_imp ni) *)
(* Goal: le (@length nested_imp ni) m *)
assumption.
(* Goal: lt (@length nested_imp ni1) (@length nested_imp ni) *)
(* Goal: le (@length nested_imp ni) m *)
apply lt_n_Sm_le; assumption.
Qed.




Lemma lt_ks_shift_nd :
 forall (ni ni1 : nested_imps) (dni dni1 : decorated_nested_imps) 
   (x : nimp) (k : kripke_tree),
 le_ni (rev_app dni1 ni1) (rev_app ((x, k) :: dni) ni) ->
 Lt_Ks ni1 dni1 (Undecorated x :: ni) dni.
(* Goal: forall (ni ni1 : nested_imps) (dni dni1 : decorated_nested_imps) (x : nimp) (k : kripke_tree) (_ : le_ni (rev_app dni1 ni1) (rev_app (@cons (prod nimp kripke_tree) (@pair nimp kripke_tree x k) dni) ni)), Lt_Ks ni1 dni1 (@cons nested_imp (Undecorated x) ni) dni *)
intros ni ni1 dni dni1 x k le.
(* Goal: Lt_Ks ni1 dni1 (@cons nested_imp (Undecorated x) ni) dni *)
apply lt_ks_count_undecs.
(* Goal: lt (@length nested_imp ni1) (@length nested_imp ni) *)
(* Goal: le (@length nested_imp ni) m *)
apply le_ni_trans with (rev_app ((x, k) :: dni) ni); try assumption.
(* Goal: le_ni (rev_app (@cons (prod nimp kripke_tree) (@pair nimp kripke_tree x k) dni) ni) (rev_app dni (@cons nested_imp (Undecorated x) ni)) *)
(* Goal: lt (count_undecs ni1) (count_undecs (@cons nested_imp (Undecorated x) ni)) *)
simpl in |- *.
(* Goal: le_ni (rev_app dni (@cons nested_imp (Decorated x k) ni)) (rev_app dni (@cons nested_imp (Undecorated x) ni)) *)
(* Goal: lt (count_undecs ni1) (count_undecs (@cons nested_imp (Undecorated x) ni)) *)
 rewrite (rev_app_app dni (Decorated x k :: ni)).
(* Goal: le_ni (@app nested_imp (rev_app dni NNil) (@cons nested_imp (Decorated x k) ni)) (rev_app dni (@cons nested_imp (Undecorated x) ni)) *)
(* Goal: lt (count_undecs ni1) (count_undecs (@cons nested_imp (Undecorated x) ni)) *)
 rewrite (rev_app_app dni (Undecorated x :: ni)).
(* Goal: le_ni (@app nested_imp (rev_app dni NNil) (@cons nested_imp (Decorated x k) ni)) (@app nested_imp (rev_app dni NNil) (@cons nested_imp (Undecorated x) ni)) *)
(* Goal: lt (count_undecs ni1) (count_undecs (@cons nested_imp (Undecorated x) ni)) *)
apply le_ni_app_dn.
(* Goal: @eq nat (@length nested_imp (rev_app dni NNil)) (@length nested_imp (rev_app dni NNil)) *)
(* Goal: le_ni (@app nested_imp (rev_app dni NNil) ni) (@app nested_imp (rev_app dni NNil) ni) *)
(* Goal: lt (count_undecs ni1) (count_undecs (@cons nested_imp (Undecorated x) ni)) *)
trivial.
(* Goal: le_ni (rev_app (@cons (prod nimp kripke_tree) (@pair nimp kripke_tree x k) dni) ni) (rev_app dni (@cons nested_imp (Decorated x k) ni)) *)
(* Goal: lt (@length nested_imp ni) (@length nested_imp (@cons nested_imp (Decorated x k) ni)) *)
apply le_ni_refl.
(* Goal: lt (count_undecs ni1) (count_undecs (@cons nested_imp (Undecorated x) ni)) *)
apply le_lt_trans with (count_undecs ni).
(* Goal: lt (@length nested_imp ni1) (@length nested_imp ni) *)
(* Goal: le (@length nested_imp ni) m *)
apply le_ks_le_count_undecs with dni1 ((x, k) :: dni); assumption.
(* Goal: lt (@length nested_imp ni1) (S (@length nested_imp ni1)) *)
(* Goal: P (rev_app dni1 ni1) *)
simpl in |- *; apply lt_n_Sn.
Qed.


Lemma lt_ks_shift_dd :
 forall (ni : nested_imps) (dni : decorated_nested_imps) 
   (x : nimp) (k : kripke_tree),
 Lt_Ks ni ((x, k) :: dni) (Decorated x k :: ni) dni.
(* Goal: forall (ni : nested_imps) (dni : decorated_nested_imps) (x : nimp) (k : kripke_tree), Lt_Ks ni (@cons (prod nimp kripke_tree) (@pair nimp kripke_tree x k) dni) (@cons nested_imp (Decorated x k) ni) dni *)
intros ni dni x k.
(* Goal: Lt_Ks ni (@cons (prod nimp kripke_tree) (@pair nimp kripke_tree x k) dni) (@cons nested_imp (Decorated x k) ni) dni *)
apply lt_ks_length.
(* Goal: le_ni (rev_app (@cons (prod nimp kripke_tree) (@pair nimp kripke_tree x k) dni) ni) (rev_app dni (@cons nested_imp (Decorated x k) ni)) *)
(* Goal: lt (@length nested_imp ni) (@length nested_imp (@cons nested_imp (Decorated x k) ni)) *)
apply le_ni_refl.
(* Goal: lt (@length nested_imp ni1) (S (@length nested_imp ni1)) *)
(* Goal: P (rev_app dni1 ni1) *)
simpl in |- *; apply lt_n_Sn.
Qed.
