Example.v

Inductive read_thread st defs : list nat -> rthreadptr -> term -> Prop :=
| read_thread_val : forall varmap rid v c t h,
    nth_error st.(st_rthreads) rid = Some {| rt_code := Val v ; rt_cont := c |} ->
    read_val st defs varmap v t ->
    read_cont st defs varmap c h ->
    read_thread st defs varmap rid (fill_hctx h t)
| read_thread_term : forall varmap rid e el c t h,
    nth_error st.(st_rthreads) rid = Some {| rt_code := Term t e ; rt_cont := c |} ->
    closed_at t (length e) ->
    Forall2 (read_val st defs varmap) e el ->
    read_cont st defs varmap c h ->
    no_dvar t ->
    read_thread st defs varmap rid (fill_hctx h (subst (read_env el) t))

with read_val st defs : list nat -> value -> term -> Prop :=
| read_val_thread :
    forall varmap rid t, read_thread st defs varmap rid t -> read_val st defs varmap (Thread rid) t
| read_val_clos :
    forall varmap t e el x vdeep tdeep,
      Forall2 (read_val st defs varmap) e el ->
      read_val st defs (x :: varmap) vdeep tdeep ->
      (* convertible beta (subst (read_env (dvar x :: el)) t) tdeep -> *)
      (* convertible beta (subst (read_env (var 0 :: el)) t) tdeep -> *)
      convertible beta (subst (lift_subst (read_env el)) t) tdeep ->
      no_dvar t -> (* Forall (dvar_free x) el -> *) length defs <= x < st.(st_freename) -> x \notin varmap ->
      closed_at t (S (length e)) ->
      read_val st defs varmap (Clos t e x vdeep) (subst (read_env el) (abs t))
| read_val_block :
    forall varmap tag e el,
      Forall2 (read_val st defs varmap) e el ->
      read_val st defs varmap (Block tag e) (constr tag el)
| read_val_neutral :
    forall varmap x c h uf tuf,
      read_cont st defs varmap c h ->
      if_Some3 (fun v2 t2 def =>
                  read_val st defs varmap v2 t2 /\
                  convertible beta (fill_hctx h def) t2 /\
                  closed_at def 0)
               uf tuf (nth_error defs x) ->
      x < st.(st_freename) ->
      (nth_error defs x = None -> In x varmap) ->
      read_val st defs varmap (Neutral (x, c, uf)) (fill_hctx h (match index Nat.eq_dec varmap x with None => dvar x | Some n => var n end))

with read_cont st defs : list nat -> cont -> hctx -> Prop :=
| read_cont_kid : forall varmap, read_cont st defs varmap Kid h_hole
| read_cont_kapp :
    forall varmap v c t h,
      read_val st defs varmap v t ->
      read_cont st defs varmap c h ->
      read_cont st defs varmap (Kapp v c) (compose_hctx h (h_app h_hole t))
| read_cont_kswitch :
    forall varmap bs e bds tdeeps c el h,
      Forall2 (read_val st defs varmap) e el ->
      read_cont st defs varmap c h ->
      Forall3
        (fun pt vdeeps tdeep =>
           length (fst vdeeps) = fst pt /\
           read_val st defs (fst vdeeps ++ varmap) (snd vdeeps) tdeep /\
           (* convertible beta (subst (read_env (map dvar (fst vdeeps) ++ el)) (snd pt)) tdeep /\ *)
           (* convertible beta (subst (read_env (map var (seq 0 (length (fst vdeeps))) ++ el)) (snd pt)) tdeep /\ *)
           convertible beta (subst (liftn_subst (fst pt) (read_env el)) (snd pt)) tdeep /\
           (* Forall (fun x => Forall (dvar_free x) el) (fst vdeeps) /\ *)
           closed_at (snd pt) (fst pt + length e) /\
           Forall (fun x => length defs <= x < st.(st_freename) /\ x \notin varmap) (fst vdeeps) /\
           NoDup (fst vdeeps) /\
           no_dvar (snd pt)
        ) bs bds tdeeps ->
      read_cont st defs varmap (Kswitch bs e bds c) (compose_hctx h (h_switch h_hole (map (fun '(p, t) => (p, subst (liftn_subst p (read_env el)) t)) bs))).

Definition read_ind st defs := Induction For [ read_thread st defs ; read_val st defs ; read_cont st defs ].

Ltac read_thread_val_intro :=
  intros varmap rid v c t h Hnth Hv Hc IHv IHc.
Ltac read_thread_term_intro :=
  intros varmap rid e el c t h Hnth Hclosed He Hc Hdv IHe IHc.
Ltac read_val_thread_intro :=
  intros varmap rid t Hrid IH.
Ltac read_val_clos_intro :=
  intros varmap t e el x vdeep tdeep He Hvdeep Hconv Hdv Hfree1 Hfree2 Hclosed IHe IHdeep.
Ltac read_val_block_intro :=
  intros varmap tag e el He IHe.
Ltac read_val_neutral_intro :=
  intros varmap x c h uf tuf Hc Huf Hfree Hin IHc IHuf.
Ltac read_cont_kid_intro :=
  intros varmap.
Ltac read_cont_kapp_intro :=
  intros varmap v c t h Hv Hc IHv IHc.
Ltac read_cont_kswitch_intro :=
  intros varmap bs e bds tdeeps c el h He Hc Hdeeps IHe IHc IHdeep.
Ltac read_ind :=
  apply read_ind; [read_thread_val_intro|read_thread_term_intro|read_val_thread_intro|read_val_clos_intro|read_val_block_intro|read_val_neutral_intro|read_cont_kid_intro|read_cont_kapp_intro|read_cont_kswitch_intro].

GenInd.v

From Ltac2 Require Import Ltac2.

Require Import List.
Require Import Rewrite.
Require Import Misc.

Ltac2 eassumption_tac () := ltac1:(eassumption).
Ltac2 Notation eassumption := eassumption_tac ().

Definition proj1_transparent {A B : Prop} (H : A /\ B) : A := match H with conj P Q => P end.
Definition proj2_transparent {A B : Prop} (H : A /\ B) : B := match H with conj P Q => Q end.

Lemma Exists_impl_transparent :
  forall (A : Type) (P Q : A -> Prop) (L : list A), (forall x, P x -> Q x) -> Exists P L -> Exists Q L.
Proof.
  intros A P Q L H1 H2. induction H2.
  - apply Exists_cons_hd, H1. assumption.
  - apply Exists_cons_tl, IHExists.
Defined.

Lemma Exists_impl_strong_transparent :
  forall (A : Type) (P Q : A -> Prop) (L : list A), (forall x, P x -> Q x) -> Exists P L -> Exists (fun x => P x /\ Q x) L.
Proof.
  intros A P Q L H1 H2. eapply Exists_impl_transparent > [|eassumption].
  intros x Hx; split > [apply Hx|apply H1, Hx].
Defined.

Lemma Forall3_impl_transparent :
  forall (A B C : Type) (P Q : A -> B -> C -> Prop) (l1 : list A) (l2 : list B) (l3 : list C), (forall x y z, P x y z -> Q x y z) -> Forall3 P l1 l2 l3 -> Forall3 Q l1 l2 l3.
Proof.
  intros A B C P Q l1 l2 l3 H1 H2; induction H2; constructor.
  - apply H1. assumption.
  - assumption.
Defined.

Inductive if_Some {A : Type} (P : A -> Prop) : option A -> Prop :=
| if_Some_None : if_Some P None
| if_Some_Some : forall x, P x -> if_Some P (Some x).

Lemma if_Some_impl_transparent :
  forall (A : Type) (P Q : A -> Prop) (x : option A), (forall x, P x -> Q x) -> if_Some P x -> if_Some Q x.
Proof.
  intros A P Q x H1 H2. inversion H2; subst.
  - constructor.
  - constructor; apply H1. assumption.
Defined.

Inductive if_Some2 {A B : Type} (P : A -> B -> Prop) : option A -> option B -> Prop :=
| if_Some2_None : if_Some2 P None None
| if_Some2_Some : forall x y, P x y -> if_Some2 P (Some x) (Some y).

Lemma if_Some2_impl_transparent :
  forall (A B : Type) (P Q : A -> B -> Prop) (x : option A) (y : option B), (forall x y, P x y -> Q x y) -> if_Some2 P x y -> if_Some2 Q x y.
Proof.
  intros A B P Q x y H1 H2. inversion H2; subst.
  - constructor.
  - constructor; apply H1. assumption.
Defined.

Inductive if_Some3 {A B C : Type} (P : A -> B -> C -> Prop) : option A -> option B -> option C -> Prop :=
| if_Some3_None : if_Some3 P None None None
| if_Some3_Some : forall x y z, P x y z -> if_Some3 P (Some x) (Some y) (Some z).

Lemma if_Some3_impl_transparent :
  forall (A B C : Type) (P Q : A -> B -> C -> Prop) (x : option A) (y : option B) (z : option C), (forall x y z, P x y z -> Q x y z) -> if_Some3 P x y z -> if_Some3 Q x y z.
Proof.
  intros A B C P Q x y z H1 H2. inversion H2; subst.
  - constructor.
  - constructor; apply H1. assumption.
Defined.


(*
Lemma exists_impl_transparent :
  forall (A : Type) (P Q : A -> Prop), (exists x, P x) -> (forall x, P x -> Q x) -> (exists x, Q x).
Proof.
  intros A P Q [x H1] H2. exists x. apply H2, H1.
Defined.

Lemma exists_impl_strong_transparent :
  forall (A : Type) (P Q : A -> Prop), (exists x, P x) -> (forall x, P x -> Q x) -> (exists x, P x /\ Q x).
Proof.
  intros A P Q H1 H2. eapply exists_impl_transparent > [eassumption|].
  intros x Hx; split > [apply Hx|apply H2, Hx].
Defined.
*)

Ltac2 msg_list_concat (l : message list) (sep : message) :=
  match l with
  | [] => Message.of_string ""
  | x :: l => List.fold_left (fun m x => Message.concat m (Message.concat sep x)) l x
  end.

Ltac2 message_concat_list (l : message list) :=
  List.fold_left (fun m1 m2 => Message.concat m1 m2) l (Message.of_string "").

Ltac2 message_of_hyps () :=
  message_concat_list (List.map (fun (id, _, c) => message_concat_list [Message.of_ident id; Message.of_string " : "; Message.of_constr c; Message.of_string "
"]) (Control.hyps ())).

Ltac2 typed_constr_message (c : constr) :=
  Message.concat (Message.concat (Message.of_constr c) (Message.of_string " : ")) (Message.of_constr (Constr.type c)).

Ltac2 msg_of_binder (b : binder) :=
  Message.concat
    (match Constr.Binder.name b with None => Message.of_string "_" | Some x => Message.of_ident x end)
    (Message.concat (Message.of_string " : ")
                    (typed_constr_message (Constr.Binder.type b))).

Ltac2 msg_of_list (l : message list) :=
  message_concat_list [Message.of_string "[" ; msg_list_concat l (Message.of_string "; "); Message.of_string "]"].

Ltac2 msg_of_array (a : message array) :=
  message_concat_list [Message.of_string "[|" ; msg_list_concat (Array.to_list a) (Message.of_string "; "); Message.of_string "|]"].

Ltac2 show_constr_kind (c : constr) :=
  let sp := Message.of_string " " in
  match Constr.Unsafe.kind c with
  | Constr.Unsafe.Rel n => Message.concat (Message.of_string "Rel ") (Message.of_int n)
  | Constr.Unsafe.Var x => Message.concat (Message.of_string "Var ") (Message.of_ident x)
  | Constr.Unsafe.Meta _ => Message.of_string "Meta _"
  | Constr.Unsafe.Evar e ca => Message.concat (Message.of_string "Evar _ ") (msg_of_array (Array.map Message.of_constr ca))
  | Constr.Unsafe.Sort _ => Message.of_string "Sort _"
  | Constr.Unsafe.Cast c1 _ c2 => message_concat_list [Message.of_string "Cast " ; Message.of_constr c1 ; Message.of_string " _ " ; Message.of_constr c2]
  | Constr.Unsafe.Prod b c => message_concat_list [Message.of_string "Prod " ; msg_of_binder b ; sp ; Message.of_constr c]
  | Constr.Unsafe.Lambda  b c => message_concat_list [Message.of_string "Lambda " ; msg_of_binder b ; sp ; Message.of_constr c]
  | Constr.Unsafe.LetIn b c1 c2 => message_concat_list [Message.of_string "LetIn " ; msg_of_binder b ; sp ; Message.of_constr c1 ; sp ; Message.of_constr c2]
  | Constr.Unsafe.App c ca => message_concat_list [Message.of_string "App " ; Message.of_constr c ; sp; msg_of_array (Array.map Message.of_constr ca)]
  | Constr.Unsafe.Constant _ _ => Message.of_string "Constant _ _"
  | Constr.Unsafe.Ind _ _ => Message.of_string "Ind _ _"
  | Constr.Unsafe.Constructor _ _ => Message.of_string "Constructor _ _"
  | Constr.Unsafe.Case _ c1 ci c2 ca => message_concat_list [Message.of_string "Case _ " ; Message.of_constr c1 ; sp ; match ci with Constr.Unsafe.NoInvert => Message.of_string "NoInvert" | Constr.Unsafe.CaseInvert ca => message_concat_list [Message.of_string "(CaseInvert "; msg_of_array (Array.map Message.of_constr ca); Message.of_string ")"] end ; sp ; Message.of_constr c2 ; sp ; msg_of_array (Array.map Message.of_constr ca) ]
  | Constr.Unsafe.Fix ia i ba ca => message_concat_list [Message.of_string "Fix "; msg_of_array (Array.map Message.of_int ia); sp ; Message.of_int i ; sp ; msg_of_array (Array.map msg_of_binder ba) ; sp ; msg_of_array (Array.map Message.of_constr ca)]
  | Constr.Unsafe.CoFix i ba ca => message_concat_list [Message.of_string "CoFix "; Message.of_int i ; sp ; msg_of_array (Array.map msg_of_binder ba) ; sp ; msg_of_array (Array.map Message.of_constr ca)]
  | Constr.Unsafe.Proj _ c => message_concat_list [Message.of_string "Proj _ "; Message.of_constr c]
  | Constr.Unsafe.Uint63 _ => Message.of_string "Uint63 _"
  | Constr.Unsafe.Float _ => Message.of_string "Float _"
  | Constr.Unsafe.Array _ ca c1 c2 => message_concat_list [Message.of_string "Array _ "; msg_of_array (Array.map Message.of_constr ca) ; sp ; Message.of_constr c1 ; sp ; Message.of_constr c2]
  end.
(*
Inductive even : nat -> Prop :=
| even_O : even O
| even_SS : forall n, even n -> even (S (S n)).
Print even_ind.
(*Fixpoint t (n : nat) (H : even n) : Prop :=
  match H return Prop with
  | even_O => n = n
  | even_SS n H1 => t n H1
  end.*)
Goal True.
  let tdef := Std.eval_cbv {Std.rBeta := true ; Std.rMatch := false ; Std.rFix := false ; Std.rCofix := false ; Std.rZeta := false ; Std.rDelta := true ; Std.rConst := []} '(even_ind (fun n => even n) even_O (fun n _ Hrec => even_SS n Hrec)) in
  Message.print (show_constr_kind tdef).
*)
Ltac2 get_binder_maybe (c : constr) :=
  match Constr.Unsafe.kind c with
  | Constr.Unsafe.Prod b _ => Some b
  | Constr.Unsafe.Lambda b _ => Some b
  | Constr.Unsafe.LetIn b _ _ => Some b
  | _ => None
  end.

Ltac2 get_binder (c : constr) :=
  match get_binder_maybe c with
  | Some b => b
  | None => Control.throw (Invalid_argument (Some (Message.of_constr c)))
  end.

Ltac2 head_binder_ident (c : constr) :=
  Fresh.in_goal (
      match get_binder_maybe c with
      | None => @_x
      | Some b =>
        match Constr.Binder.name b with
        | None => @_x
        | Some x => x
        end
      end).

Ltac2 rec rebuild_lam (t : constr) :=
  match Constr.Unsafe.kind t with
  | Constr.Unsafe.Lambda b t1 => Constr.Unsafe.make (Constr.Unsafe.Lambda b (rebuild_lam t1))
  | _ => t
  end.

Ltac2 rec rebuild_prod_cast (t : constr) :=
  match Constr.Unsafe.kind t with
  | Constr.Unsafe.Prod b t1 => Constr.Unsafe.make (Constr.Unsafe.Prod b (rebuild_prod_cast t1))
  | Constr.Unsafe.Lambda b t1 => Constr.Unsafe.make (Constr.Unsafe.Lambda b (rebuild_prod_cast t1))
  | Constr.Unsafe.Cast t1 _ _ => rebuild_prod_cast t1
  | _ => t
  end.

Ltac2 force_prop (tac : unit -> constr) :=
  '(ltac2:(Control.refine tac) : Prop).
Ltac2 force_prop_t (tac : unit -> constr) :=
  '(ltac2:(Control.refine tac) : _ : Prop).

Ltac2 inctx (name : ident) (t : constr) (body : constr -> constr) :=
  rebuild_lam (Constr.in_context name t (fun () => Control.refine (fun () => body (Control.hyp name)))).
Ltac2 inctx_p (name : ident) (t : constr) (body : constr -> constr) :=
  force_prop_t (fun () => inctx name t body).

Ltac2 make_forall (c : constr) :=
  match Constr.Unsafe.kind c with
  | Constr.Unsafe.Lambda b t => Constr.Unsafe.make (Constr.Unsafe.Prod b t)
  | _ => Control.throw (Invalid_argument (Some (Message.of_constr c)))
  end.

Ltac2 mk_app (u : constr) (v : constr) := '($u $v).
Ltac2 mk_app2 (u : constr) (v : constr) (w : constr) := '($u $v $w).
Ltac2 mk_app3 (u : constr) (v : constr) (w : constr) (x : constr) := '($u $v $w $x).

Ltac2 mk_forall_proof_smart (x : ident) (u : constr) (v : constr -> constr) :=
  lazy_match! (Std.eval_hnf u) with
  | True => v 'I
  | ?u =>
    let vx := inctx_p x u v in
    lazy_match! (Std.eval_hnf (Constr.type vx)) with
    | (_ -> True) => 'I
    | _ => vx
    end
  end.

Ltac2 mk_Forall_proof_smart (x : ident) (t : constr) (u : constr -> constr) (v : constr) :=
  let ux := inctx_p x t u in
  lazy_match! (Std.eval_hnf (Constr.type ux)) with
  | (_ -> True) => 'I
  | _ => '(Forall_True_transparent $t _ $v $ux)
  end.

Ltac2 mk_and_proof_smart (u : constr) (v : constr) :=
  let ut := Std.eval_hnf (Constr.type u) in
  let vt := Std.eval_hnf (Constr.type v) in
  lazy_match! '($ut /\ $vt) with
  | True /\ _ => v
  | _ /\ True => u
  | _ => '(conj $u $v)
  end.


Ltac2 mk_Forall_impl_smart (t : constr) (p : constr) (l : constr) (u : constr -> constr) (v : constr) :=
  let ux := inctx_p (head_binder_ident p) t (fun xx => inctx (Fresh.in_goal @H) (mk_app p xx) u) in
  lazy_match! (Std.eval_hnf (Constr.type ux)) with
  | (forall x H, True) => 'I
  | _ => '(Forall_impl_transparent $t _ _ $l $ux $v)
  end.

Ltac2 mk_Forall2_impl_smart (t1 : constr) (t2 : constr) (p : constr) (l1 : constr) (l2 : constr) (u : constr -> constr) (v : constr) :=
  let ux := inctx_p (head_binder_ident p) t1 (fun xx =>
    let y := head_binder_ident (Std.eval_hnf (mk_app p xx)) in
    inctx_p y t2 (fun yy =>
      inctx_p (Fresh.in_goal @H) (mk_app (mk_app p xx) yy) u)) in
  lazy_match! (Std.eval_hnf (Constr.type ux)) with
  | (forall x y H, True) => 'I
  | _ => '(Forall2_impl_transparent $t1 $t2 _ _ $l1 $l2 $ux $v)
  end.

Ltac2 mk_Forall3_impl_smart (t1 : constr) (t2 : constr) (t3 : constr) (p : constr) (l1 : constr) (l2 : constr) (l3 : constr) (u : constr -> constr) (v : constr) :=
  let ux := inctx_p (head_binder_ident p) t1 (fun xx =>
    let y := head_binder_ident (Std.eval_hnf (mk_app p xx)) in
    inctx_p y t2 (fun yy =>
      let z := head_binder_ident (Std.eval_hnf (mk_app (mk_app p xx) yy)) in
      inctx_p z t3 (fun zz =>
        inctx_p (Fresh.in_goal @H) (mk_app (mk_app (mk_app p xx) yy) zz) u))) in
  lazy_match! (Std.eval_hnf (Constr.type ux)) with
  | (forall x y z H, True) => 'I
  | _ => '(Forall3_impl_transparent $t1 $t2 $t3 _ _ $l1 $l2 $l3 $ux $v)
  end.

Ltac2 mk_if_Some_impl_smart (t : constr) (p : constr) (o : constr) (u : constr -> constr) (v : constr) :=
  let ux := inctx_p (head_binder_ident p) t (fun xx => inctx (Fresh.in_goal @H) (mk_app p xx) u) in
  lazy_match! (Std.eval_hnf (Constr.type ux)) with
  | (forall x H, True) => 'I
  | _ => '(if_Some_impl_transparent $t _ _ $o $ux $v)
  end.

Ltac2 mk_if_Some2_impl_smart (t1 : constr) (t2 : constr) (p : constr) (o1 : constr) (o2 : constr) (u : constr -> constr) (v : constr) :=
  let ux := inctx_p (head_binder_ident p) t1 (fun xx =>
    let y := head_binder_ident (Std.eval_hnf (mk_app p xx)) in
    inctx_p y t2 (fun yy =>
      inctx_p (Fresh.in_goal @H) (mk_app (mk_app p xx) yy) u)) in
  lazy_match! (Std.eval_hnf (Constr.type ux)) with
  | (forall x y H, True) => 'I
  | _ => '(if_Some2_impl_transparent $t1 $t2 _ _ $o1 $o2 $ux $v)
  end.

Ltac2 mk_if_Some3_impl_smart (t1 : constr) (t2 : constr) (t3 : constr) (p : constr) (o1 : constr) (o2 : constr) (o3 : constr) (u : constr -> constr) (v : constr) :=
  let ux := inctx_p (head_binder_ident p) t1 (fun xx =>
    let y := head_binder_ident (Std.eval_hnf (mk_app p xx)) in
    inctx_p y t2 (fun yy =>
      let z := head_binder_ident (Std.eval_hnf (mk_app (mk_app p xx) yy)) in
      inctx_p z t3 (fun zz =>
        inctx_p (Fresh.in_goal @H) (mk_app (mk_app (mk_app p xx) yy) zz) u))) in
  lazy_match! (Std.eval_hnf (Constr.type ux)) with
  | (forall x y z H, True) => 'I
  | _ => '(if_Some3_impl_transparent $t1 $t2 $t3 _ _ $o1 $o2 $o3 $ux $v)
  end.


Ltac2 mk_step_one_impl_smart (t : constr) (r : constr) (l1 : constr) (l2 : constr) (u : constr -> constr) (v : constr) :=
  let ux := inctx_p (head_binder_ident r) t (fun xx =>
    let y := head_binder_ident (Std.eval_hnf (mk_app r xx)) in
    inctx_p y t (fun yy =>
      inctx_p (Fresh.in_goal @H) (mk_app (mk_app r xx) yy) u)) in
  lazy_match! (Std.eval_hnf (Constr.type ux)) with
  | (forall x y H, True) => 'I
  | _ => '(step_one_impl_strong_transparent $t _ _ $l1 $l2 $ux $v)
  end.

Ltac2 mk_Exists_impl_smart (t : constr) (p : constr) (l : constr) (u : constr -> constr) (v : constr) :=
  let ux := inctx_p (head_binder_ident p) t (fun xx => inctx (Fresh.in_goal @H) (mk_app p xx) u) in
  lazy_match! (Std.eval_hnf (Constr.type ux)) with
  | (forall x H, True) => 'I
  | _ => '(Exists_impl_strong_transparent $t _ _ $l $ux $v)
  end.

(*
Ltac2 mk_exists_impl_smart (t : constr) (p : constr) (u : constr -> constr) (v : constr) :=
  let ux := inctx_p (head_binder_ident p) t (fun xx => inctx (Fresh.in_goal @H) (mk_app p xx) u) in
  lazy_match! (Std.eval_hnf (Constr.type ux)) with
  | (forall x H, True) => 'I
  | _ => '(exists_impl_strong_transparent $t _ _ $ux $v)
  end.
 *)


Ltac2 log (c : constr) := Message.print (typed_constr_message c).
Ltac2 logged (r : constr) := log r; r.
Ltac2 log_context () := Message.print (Message.of_string "Context:"); Message.print (message_of_hyps ()).

Ltac2 rec is_ind_prefix (ind : constr) (t : constr) (args : constr list) :=
  (* Assumes t is in hnf *)
  if Constr.equal t ind then
    Some (List.rev args)
  else
    lazy_match! t with
    | ?t1 ?t2 => is_ind_prefix ind t1 (t2 :: args)
    | _ => None
    end.

Ltac2 rec is_ind_prefix_l (inds : constr list) (t : constr) (l : 'a list) :=
  match inds with
  | [] => None
  | ind :: inds =>
    match is_ind_prefix ind t [] with
    | Some args => Some (args, List.hd l)
    | None => is_ind_prefix_l inds t (List.tl l)
    end
  end.

Ltac2 rec applist (c : constr) (l : constr list) :=
  match l with
  | [] => c
  | x :: l => mk_app (applist c l) x
  end.

Ltac2 rec constrind_hyp (v : constr) (inds : constr list) (hrecs : constr list) :=
  let t := Std.eval_hnf (Constr.type v) in
  match is_ind_prefix_l inds t hrecs with
  | Some argshrec => let (args, hrec) := argshrec in mk_app (applist hrec args) v
  | None =>
    lazy_match! t with
    | list ?a => mk_Forall_proof_smart (Fresh.in_goal @x) a (fun x => constrind_hyp x inds hrecs) v
    | @Forall ?t ?p ?l =>
      mk_Forall_impl_smart t p l (fun h => constrind_hyp h inds hrecs) v
    | @Forall2 ?t1 ?t2 ?p ?l1 ?l2 =>
      mk_Forall2_impl_smart t1 t2 p l1 l2 (fun h => constrind_hyp h inds hrecs) v
    | @Forall3 ?t1 ?t2 ?t3 ?p ?l1 ?l2 ?l3 =>
      mk_Forall3_impl_smart t1 t2 t3 p l1 l2 l3 (fun h => constrind_hyp h inds hrecs) v
    | @if_Some ?t ?p ?x =>
      mk_if_Some_impl_smart t p x (fun h => constrind_hyp h inds hrecs) v
    | @if_Some2 ?t1 ?t2 ?p ?x ?y =>
      mk_if_Some2_impl_smart t1 t2 p x y (fun h => constrind_hyp h inds hrecs) v
    | @if_Some3 ?t1 ?t2 ?t3 ?p ?x ?y ?z =>
      mk_if_Some3_impl_smart t1 t2 t3 p x y z (fun h => constrind_hyp h inds hrecs) v
    | @step_one ?t ?r ?l1 ?l2 =>
      mk_step_one_impl_smart t r l1 l2 (fun h => constrind_hyp h inds hrecs) v
    | @Exists ?t ?p ?l =>
      mk_Exists_impl_smart t p l (fun h => constrind_hyp h inds hrecs) v
(*    | @ex ?t ?p =>
      mk_exists_impl_smart t p (fun h => constrind_hyp h inds hrecs) v *)
    | (?a * ?b)%type =>
      mk_and_proof_smart
        (constrind_hyp (mk_app 'fst v) inds hrecs)
        (constrind_hyp (mk_app 'snd v) inds hrecs)
    | ?a /\ ?b =>
      mk_and_proof_smart
        (constrind_hyp (mk_app 'proj1_transparent v) inds hrecs)
        (constrind_hyp (mk_app 'proj2_transparent v) inds hrecs)
    | forall (x : ?t1), @?t2 x =>
      mk_forall_proof_smart (head_binder_ident t) t1 (fun x => constrind_hyp (mk_app v x) inds hrecs)
    | _ => 'I
    end
  end.

Ltac2 add1 (t : constr) (l : constr list) :=
  lazy_match! (Std.eval_hnf (Constr.type t)) with
  | True => l
  | _ => t :: l
  end.

Ltac2 maybe_app (t1 : constr) (t2 : constr) :=
  lazy_match! (Constr.type (Constr.type t2)) with
  | Prop => t1
  | _ => mk_app t1 t2
  end.

Ltac2 rec constrind1 (c : constr) (cstr : constr) (cstrhyp : constr) (inds : constr list) (ps : constr list) (hrecs : constr list) (args : constr list) (args_recs : constr list) :=
  let c := Std.eval_hnf c in
  lazy_match! c with
  | forall (x : ?t1), @?t2 x =>
    let x := head_binder_ident c in
    inctx_p x t1 (fun xx =>
      constrind1 (mk_app t2 xx) cstr cstrhyp inds ps hrecs (xx :: args) (add1 (constrind_hyp xx inds hrecs) args_recs)
    )
  | ?c =>
    let nt := applist (applist cstrhyp args) args_recs in
    match is_ind_prefix_l inds (Constr.type (applist cstr args)) ps with
    | None => Control.throw Assertion_failure
    | Some targsp =>
      let (targs, p) := targsp in
      Std.unify (Constr.type nt) (maybe_app (applist p targs) (applist cstr args));
      nt
    end
  end.

Ltac2 get_constructors_base (ind : inductive) (inst : instance) (args : constr list) :=
  List.init (Ind.nconstructors (Ind.data ind))
            (fun i => let c := Ind.get_constructor (Ind.data ind) i in
                   applist (Constr.Unsafe.make (Constr.Unsafe.Constructor c inst)) (List.rev args)
            ).

Ltac2 rec split_ind (c : constr) (args : constr list) :=
  lazy_match! (Std.eval_hnf c) with
  | ?t1 ?t2 => split_ind t1 (t2 :: args)
  | ?c => match Constr.Unsafe.kind c with
         | Constr.Unsafe.Ind ind inst => (ind, inst, args)
         | _ => Control.throw (Invalid_argument (Some (Message.of_constr c)))
         end
  end.

Ltac2 get_constructors (c : constr) :=
  let (ind, inst, args) := split_ind c [] in
  get_constructors_base ind inst args.

(*
Ltac2 rec copy_string_from (s1 : string) (s2 : string) (i : int) (j : int) :=
  if Int.equal i (String.length s1) then () else (
      String.set s2 j (String.get s1 i);
      copy_string_from s1 s2 (Int.add i 1) (Int.add j 1)
    ).

Ltac2 concat_string (s1 : string) (s2 : string) :=
  let s3 := String.make (Int.add (String.length s1) (String.length s2)) (Char.of_int 0) in
  copy_string_from s1 s3 0 0;
  copy_string_from s2 s3 0 (String.length s1);
  s3.

Ltac2 named_ident (s : string) := match Ident.of_string s with Some i => i | None => @_unnamed_ end.
 *)

Ltac2 rec ncontext (l : constr list) (l2 : constr list) (tac : constr list -> constr) :=
  match l with
  | [] => tac (List.rev l2)
  | _ :: l => inctx_p (Fresh.in_goal @H) '(_ : Prop) (fun h => ncontext l (h :: l2) tac)
  end.

Ltac2 rec nabs (n : int) (c : constr) :=
  if Int.equal n 0 then c else '(fun _ => ltac2:(Control.refine (fun () => nabs (Int.sub n 1) c))).

Ltac2 rec ind_principle_p (t : constr) :=
  lazy_match! (Constr.type t) with
  | forall (x : ?t1), _ =>
    let x := head_binder_ident (Constr.type t) in
    make_forall (inctx x t1 (fun xx => ind_principle_p (mk_app t xx)))
  | Set => '(($t -> Prop) : Prop)
  | Type => '(($t -> Prop) : Prop)
  | Prop => 'Prop
  end.

Ltac2 rec forall_principle (t : constr) (p : constr) :=
  force_prop (fun () =>
  lazy_match! (Constr.type t) with
  | forall (x : ?t1), _ =>
    let x := head_binder_ident (Constr.type t) in
    make_forall (inctx x t1 (fun xx => forall_principle (mk_app t xx) (mk_app p xx)))
  | Set => '(forall (t : $t), $p t)
  | Type => '(forall (t : $t), $p t)
  | Prop => '(($t -> $p) : Prop)
  end).

Ltac2 rec intro_hyp (name : ident) (c : constr) (tac : constr -> constr) :=
  force_prop_t (fun () =>
  lazy_match! (Constr.type c) with
  | forall (x : ?t1), _ =>
    inctx (head_binder_ident (Constr.type c)) t1 (fun xx => intro_hyp name (mk_app c xx) tac)
  | _ => inctx name c tac
  end).

Ltac2 rec rec_pos (t : constr) :=
  match Constr.Unsafe.kind t with
  | Constr.Unsafe.Prod _ t => Int.add 1 (rec_pos t)
  | _ => 0
  end.

Ltac2 rec eta_expand (c : constr) (p : constr) :=
  lazy_match! (Constr.type c) with
  | forall (x : ?t1), _ =>
    let x := head_binder_ident (Constr.type c) in
    inctx x t1 (fun xx => eta_expand (mk_app c xx) (mk_app p xx))
  | Prop => '(fun (_ : $c) => $p)
  | Set => '(fun (t : $c) => $p t)
  | Type => '(fun (t : $c) => $p t)
  end.

Ltac2 rec fresh_n (n : int) (x : ident) (s : Fresh.Free.t) :=
  if Int.equal n 0 then [] else
    let y := Fresh.fresh s x in
    y :: fresh_n (Int.sub n 1) x (Fresh.Free.union s (Fresh.Free.of_ids [y])).

Ltac2 rec fresh_n_goal (n : int) (x : ident) := fresh_n n x (Fresh.Free.of_goal ()).

Ltac2 inctxn (names : ident list) (ts : constr list) (body : constr list -> constr) :=
  List.fold_right2 (fun name t tac l => inctx name t (fun x => tac (x :: l))) (fun l => body (List.rev l)) names ts [].

Ltac2 ncontext_l (cstrsl : constr list list) (body : constr list list -> constr) :=
  List.fold_right (fun cstrs tac lhl => ncontext cstrs [] (fun lhyps => tac (lhyps :: lhl))) (fun l => body (List.rev l)) cstrsl [].

Ltac2 mkfix1 (guarded_arg : int) (name : ident) (t : constr) (body : constr -> constr) :=
  let (b, body) :=
      match Constr.Unsafe.kind (inctx name t body) with
      | Constr.Unsafe.Lambda b body => (b, body)
      | _ => Control.throw Assertion_failure
      end
  in
  Constr.Unsafe.make (Constr.Unsafe.Fix (Array.make 1 guarded_arg) 0 (Array.make 1 b) (Array.make 1 body)).

Ltac2 rec get_body (names : ident list) (bds : binder list) (t : constr) :=
  match names with
  | [] => (List.rev bds, t)
  | _ :: names =>
    match Constr.Unsafe.kind t with
    | Constr.Unsafe.Lambda b body => get_body names (b :: bds) body
    | _ => Control.throw Assertion_failure
    end
  end.

(* Ltac2 mkprod u v := '(conj _ _ $u $v). *)
Ltac2 mkprod u v :=
  '(conj $u $v).

Ltac2 rec mkprodn (l : constr list) :=
  match List.tl l with
  | [] => List.hd l
  | _ => mkprod (List.hd l) (mkprodn (List.tl l))
  end.

Ltac2 rotate_left (l : 'a list) (n : int) :=
  List.append (List.skipn n l) (List.firstn n l).
Ltac2 rotate_right (l : 'a list) (n : int) :=
  rotate_left l (Int.sub (List.length l) n).

Ltac2 mkfix_one (guarded_arg : int list) (names : ident list) (ts : constr list) (body : (constr list -> constr) list) (n : int) :=
  let ts := List.map rebuild_prod_cast ts in
  let bodies := List.map rebuild_prod_cast (List.map (inctxn names ts) body) in
  (* List.iter Message.print (List.map show_constr_kind ts);
  List.iter log ts; List.iter log (List.map Constr.type bodies); *)
  let (binders, _) := get_body names [] (List.hd bodies) in
  let binders := Array.of_list binders in
  let guarded_arg := Array.of_list guarded_arg in
  let bodies := Array.of_list (List.map (fun body => let (_, body) := (get_body names [] body) in body) bodies) in
  Constr.Unsafe.make (Constr.Unsafe.Fix guarded_arg n binders bodies).

Ltac2 mkfix_one' (guarded_arg : int list) (names : ident list) (ts : constr list) (body : (constr list -> constr) list) (n : int) :=
  mkfix_one (rotate_left guarded_arg n) (rotate_left names n) (rotate_left ts n) (rotate_left (List.map (fun f l => f (rotate_right l n)) body) n) 0.

Ltac2 mkfix (guarded_arg : int list) (names : ident list) (ts : constr list) (body : (constr list -> constr) list) :=
  mkprodn (List.init (List.length names) (fun n => mkfix_one guarded_arg names ts body n)).

Ltac2 map3 f l1 l2 l3 := List.map2 (fun a (b, c) => f a b c) l1 (List.combine l2 l3).
Ltac2 map4 f l1 l2 l3 l4 := map3 (fun a b (c, d) => f a b c d) l1 l2 (List.combine l3 l4).
Ltac2 map5 f l1 l2 l3 l4 l5 := map4 (fun a b c (d, e) => f a b c d e) l1 l2 l3 (List.combine l4 l5).

Ltac2 gen_ind_principle (cl : constr list) :=
  let n := List.length cl in
  let indstl := List.map (fun c => split_ind c []) cl in
  let cstrsl := List.map (fun (ind, inst, args) => get_constructors_base ind inst args) indstl in
  inctxn (fresh_n_goal n @P) (List.map ind_principle_p cl) (fun pl =>
    ncontext_l cstrsl (fun lhypsl =>
      mkfix (List.map (fun c => rec_pos (Constr.type c)) cl) (fresh_n_goal n @Hrec) (List.map2 forall_principle cl pl)
            (map5 (fun c (ind, _, _) => fun p cstrs lhyps hrecs =>
        intro_hyp (Fresh.in_goal @x) c (fun xx =>
          let branches := List.map2 (fun cstr hcstr => force_prop_t (fun () => rebuild_lam (constrind1 (Constr.type cstr) cstr hcstr cl pl hrecs [] []))) cstrs lhyps in
          (* log (rebuild_lam (eta_expand c p)); *)
          force_prop_t (fun () => Constr.Unsafe.make
            (Constr.Unsafe.Case
               (Constr.Unsafe.case ind)
               (rebuild_lam (eta_expand c p))
               Constr.Unsafe.NoInvert
               xx
               (Array.of_list branches)))
         )) cl indstl pl cstrsl lhypsl)
    )
  ).

Notation "'Induction' 'For' [ x ]" := ltac2:(let l := [x] in Control.refine (fun () => gen_ind_principle (List.map Constr.pretype l))) (at level 0, only parsing).
Notation "'Induction' 'For' [ x ; y ]" :=
  ltac2:(let l := [x; y] in Control.refine (fun () => gen_ind_principle (List.map Constr.pretype l))) (at level 0, only parsing).
Notation "'Induction' 'For' [ x ; y ; z ]" :=
  ltac2:(let l := [x; y; z] in Control.refine (fun () => gen_ind_principle (List.map Constr.pretype l))) (at level 0, only parsing).
Notation "'Induction' 'For' [ x ; y ; z ; w ]" :=
  ltac2:(let l := [x; y; z; w] in Control.refine (fun () => gen_ind_principle (List.map Constr.pretype l))) (at level 0, only parsing).
Notation "'Induction' 'For' [ x ; y ; z ; w ; t ]" :=
  ltac2:(let l := [x; y; z; w; t] in Control.refine (fun () => gen_ind_principle (List.map Constr.pretype l))) (at level 0, only parsing).

(*
Inductive even : nat -> Prop :=
| even_O : even O
| even_SS : forall n, even n -> even (S (S n)).
Definition a := Induction For [ even ].
Definition b := a even even_O (fun n _ Hrec => even_SS n Hrec).
Check b.
Goal True.

  log (Constr.type 'b).

Check (forall (x : nat), Prop).
*)

Misc.v

Require Import List.
Require Import Setoid.
Require Import Morphisms.
Require Import Arith.
Require Import Psatz.
Require Import Coq.Logic.Eqdep_dec.

Lemma Some_inj : forall A (x y : A), Some x = Some y -> x = y.
Proof.
  intros; congruence.
Qed.
Ltac autoinjSome :=
  repeat match goal with
           [ H : Some ?x = Some ?y |- _ ] => apply Some_inj in H; subst
         end.

(* List Notations *)

Notation "x '\in' L" := (In x L) (at level 80, only parsing).
Notation "x '\notin' L" := (~ In x L) (at level 80, only parsing).
Notation "x ∈ L" := (x \in L) (at level 80).
Notation "x ∉ L" := (x \notin L) (at level 80).

Fixpoint index {A : Type} (dec : forall x y : A, {x = y} + {x <> y}) L x :=
  match L with
  | nil => None
  | y :: L => if dec x y then Some 0 else option_map S (index dec L x)
  end.

Lemma index_notin_None :
  forall A eq_dec (l : list A) (x : A), x \notin l -> index eq_dec l x = None.
Proof.
  intros A eq_dec l x H; induction l.
  - reflexivity.
  - simpl in *. destruct eq_dec; [intuition congruence|].
    rewrite IHl; tauto.
Qed.

Lemma index_app :
  forall A eq_dec (l1 l2 : list A) x,
    index eq_dec (l1 ++ l2) x =
    match index eq_dec l1 x with
    | Some n => Some n
    | None => option_map (fun n => length l1 + n) (index eq_dec l2 x)
    end.
Proof.
  intros A eq_dec l1 l2 x; induction l1; simpl in *.
  - destruct index; reflexivity.
  - destruct eq_dec; [reflexivity|].
    rewrite IHl1. destruct (index eq_dec l1 x); [reflexivity|].
    destruct (index eq_dec l2 x); reflexivity.
Qed.

Lemma index_in_Some :
  forall A eq_dec (l : list A) (x : A), x \in l -> exists k, index eq_dec l x = Some k.
Proof.
  intros A eq_dec l x H; induction l.
  - simpl in *; tauto.
  - simpl. destruct eq_dec; [exists 0; reflexivity|].
    destruct IHl as (k & Hk).
    + destruct H; [symmetry in H|]; tauto.
    + exists (S k). rewrite Hk; reflexivity.
Qed.

Lemma index_in_not_None :
  forall A eq_dec (l : list A) (x : A), x \in l -> index eq_dec l x <> None.
Proof.
  intros A eq_dec l x H. destruct (index_in_Some A eq_dec l x H) as (k & Hk). congruence.
Qed.

Lemma nth_error_index :
  forall A eq_dec (x : A) l n, index eq_dec l x = Some n -> nth_error l n = Some x.
Proof.
  intros A eq_dec x. induction l; intros [|n]; simpl in *; try congruence; destruct eq_dec; simpl in *; try congruence.
  - destruct index; simpl; congruence.
  - destruct index; simpl; [|congruence]. intros; apply IHl; congruence.
Qed.

Lemma index_nth_error :
  forall (A : Type) eq_dec (vars : list A) k x, NoDup vars -> nth_error vars k = Some x -> index eq_dec vars x = Some k.
Proof.
  intros A eq_dec vars k x H1 H2. revert k H2; induction vars as [|y vars]; intros k H2; simpl in *.
  - destruct k; simpl in *; congruence.
  - destruct k; simpl in *.
    + injection H2 as H2; subst. destruct eq_dec; [|tauto]. reflexivity.
    + destruct eq_dec; [subst|].
      * inversion H1; subst. exfalso. apply H3. eapply nth_error_In; eassumption.
      * erewrite IHvars; [reflexivity| |eassumption].
        inversion H1; subst; assumption.
Qed.

Lemma index_seq :
  forall eq_dec a len x,
    a <= x < a + len ->
    index eq_dec (seq a len) x = Some (x - a).
Proof.
  intros eq_dec a len x Hx. revert a Hx; induction len; intros a Hx.
  - lia.
  - simpl index. destruct eq_dec.
    + subst. f_equal. lia.
    + rewrite IHlen; [|lia]. simpl. f_equal. lia.
Qed.

Lemma index_length :
  forall A eq_dec (x : A) l n, index eq_dec l x = Some n -> n < length l.
Proof.
  induction l; intros n Hn; simpl in *.
  - congruence.
  - destruct eq_dec; [injection Hn as Hn; lia|].
    destruct index eqn:Hidx; simpl in *; [|congruence].
    specialize (IHl n1 eq_refl). injection Hn as Hn; lia.
Qed.

Lemma nth_error_map :
  forall (A B : Type) (f : A -> B) L n, nth_error (map f L) n = match nth_error L n with Some x => Some (f x) | None => None end.
Proof.
  intros A B f L. induction L as [|a L]; intros [|n]; simpl; try reflexivity.
  apply IHL.
Qed.

Lemma nth_error_decompose :
  forall (A : Type) (L : list A) x n, nth_error L n = Some x -> exists L1 L2, L = L1 ++ x :: L2 /\ length L1 = n.
Proof.
  intros A L. induction L as [|y L]; intros x [|n] H; simpl in *; try congruence; autoinjSome.
  - exists nil. exists L. split; reflexivity.
  - apply IHL in H. destruct H as (L1 & L2 & H1 & H2). exists (y :: L1). exists L2.
    split; [rewrite H1; reflexivity|simpl; rewrite H2; reflexivity].
Qed.

Lemma nth_error_Some2 :
  forall (A : Type) (l : list A) n, n < length l -> exists x, nth_error l n = Some x.
Proof.
  intros A l n. revert l; induction n; intros l H; destruct l as [|x l]; simpl in *; try lia.
  - exists x. reflexivity.
  - apply IHn. lia.
Qed.

Lemma nth_error_Some3 :
  forall (A : Type) (l : list A) n x, nth_error l n = Some x -> n < length l.
Proof.
  intros. apply nth_error_Some. destruct nth_error; congruence.
Qed.

Lemma nth_error_app_Some :
  forall (A : Type) (l1 l2 : list A) k x, nth_error l1 k = Some x -> nth_error (l1 ++ l2) k = Some x.
Proof.
  induction l1; intros l2 [|k] x; simpl in *; intros; try congruence.
  apply IHl1; assumption.
Qed.

Lemma nth_error_extend :
  forall {A : Type} (l : list A) x, nth_error (l ++ x :: nil) (length l) = Some x.
Proof.
  intros A l x. rewrite nth_error_app2 by lia.
  destruct (length l - length l) eqn:Hll; [reflexivity|lia].
Qed.

Lemma nth_error_extend_case :
  forall {A : Type} l (x : A) n,
    nth_error (l ++ x :: nil) n = nth_error l n \/ (n = length l /\ nth_error (l ++ x :: nil) n = Some x).
Proof.
  intros A l x n.
  destruct (le_lt_dec (length l) n).
  - rewrite nth_error_app2 by assumption.
    destruct (n - length l) eqn:Hn; simpl; [right; split; [lia|reflexivity]|].
    left. destruct n0; symmetry; apply nth_error_None; assumption.
  - left. rewrite nth_error_app1; tauto.
Qed.

Definition nth_error_None_rw :
  forall {A : Type} (l : list A) (n : nat), length l <= n -> nth_error l n = None.
Proof.
  intros. apply nth_error_None. assumption.
Qed.

Lemma nth_error_select :
  forall (A : Type) (l1 l2 : list A) (x : A), nth_error (l1 ++ x :: l2) (length l1) = Some x.
Proof.
  intros; induction l1; simpl in *; [reflexivity|assumption].
Qed.


Lemma list_exists :
  forall (A : Type) (P : nat -> A -> Prop) n, (forall k, k < n -> exists x, P k x) -> exists L, length L = n /\ (forall k x, nth_error L k = Some x -> P k x).
Proof.
  intros A P n. induction n; intros H.
  - exists nil. split; [reflexivity|].
    intros [|k]; simpl; intros; discriminate.
  - destruct IHn as [L HL]; [intros k Hk; apply H; lia|].
    destruct (H n) as [x Hx]; [lia|].
    exists (L ++ x :: nil). split.
    + rewrite app_length; simpl. lia.
    + intros k y.
      destruct (le_lt_dec n k).
      * rewrite nth_error_app2 by lia.
        destruct (k - length L) as [|u] eqn:Hu; simpl.
        -- assert (k = n) by lia. congruence.
        -- destruct u; simpl; discriminate.
      * rewrite nth_error_app1 by lia. apply HL.
Qed.

Lemma list_app_eq_length :
  forall A (l1 l2 l3 l4 : list A), l1 ++ l3 = l2 ++ l4 -> length l1 = length l2 -> l1 = l2 /\ l3 = l4.
Proof.
  intros A l1 l2 l3 l4; revert l2; induction l1; intros l2 H1 H2; destruct l2; simpl in *; try intuition congruence.
  specialize (IHl1 l2 ltac:(congruence) ltac:(congruence)).
  intuition congruence.
Qed.

Lemma list_select_eq :
  forall (A : Type) (l1a l1b l2a l2b : list A) (x1 x2 : A),
    l1a ++ x1 :: l1b = l2a ++ x2 :: l2b ->
    (l1a = l2a /\ x1 = x2 /\ l1b = l2b) \/
    (exists l3, l1a ++ x1 :: l3 = l2a /\ l1b = l3 ++ x2 :: l2b) \/
    (exists l3, l1a = l2a ++ x2 :: l3 /\ l3 ++ x1 :: l1b = l2b).
Proof.
  intros A l1a. induction l1a as [|x1a l1a IH]; intros l1b l2a l2b x1 x2 Heq; destruct l2a as [|x2a l2a]; simpl in *.
  - left. split; [reflexivity|].
    split; congruence.
  - right. left. exists l2a. split; congruence.
  - right. right. exists l1a. split; congruence.
  - specialize (IH l1b l2a l2b x1 x2 ltac:(congruence)).
    destruct IH as [IH | [IH | IH]]; [left|right; left|right; right].
    + intuition congruence.
    + destruct IH as (l3 & H1 & H2). exists l3. intuition congruence.
    + destruct IH as (l3 & H1 & H2). exists l3. intuition congruence.
Qed.

Lemma select2_app_assoc :
  forall (A : Type) (l1 l2 l3 : list A) (x1 x2 : A),
    (l1 ++ x1 :: l2) ++ x2 :: l3 = l1 ++ x1 :: l2 ++ x2 :: l3.
Proof.
  intros.
  rewrite <- app_assoc. reflexivity.
Qed.

Lemma length_select :
  forall (A : Type) (l1 l2 : list A) (x1 x2 : A),
    length (l1 ++ x1 :: l2) = length (l1 ++ x2 :: l2).
Proof.
  intros; rewrite !app_length; reflexivity.
Qed.


(* Map for association lists *)

Definition map_assq {A B C : Type} (f : A -> B -> C) (L : list (A * B)) := map (fun '(x, u) => (x, f x u)) L.

Lemma map_assq_id_forall :
  forall (A B : Type) (f : A -> B -> B) (L : list (A * B)), Forall (fun '(x, u) => f x u = u) L -> map_assq f L = L.
Proof.
  intros A B f L H. induction L as [|[x u] L].
  - reflexivity.
  - inversion H; subst.
    simpl. f_equal.
    + congruence.
    + auto.
Qed.

Lemma map_assq_compose :
  forall {A B C D : Type} (f : A -> B -> C) (g : A -> C -> D) L, map_assq g (map_assq f L) = map_assq (fun x u => g x (f x u)) L.
Proof.
  intros. unfold map_assq. rewrite map_map. apply map_ext.
  intros [? ?]; simpl; reflexivity.
Qed.

Lemma map_assq_length :
  forall {A B C : Type} (f : A -> B -> C) L, length (map_assq f L) = length L.
Proof.
  intros; unfold map_assq; rewrite map_length; reflexivity.
Qed.

Lemma map_assq_ext :
  forall {A B C : Type} (f g : A -> B -> C) L, (forall x u, f x u = g x u) -> map_assq f L = map_assq g L.
Proof.
  intros; unfold map_assq; apply map_ext; intros [? ?]; f_equal; auto.
Qed.

(* Theorems on Forall *)

Lemma Forall_cons_iff :
  forall A (P : A -> Prop) a L, Forall P (a :: L) <-> P a /\ Forall P L.
Proof.
  intros. split.
  - intros H; inversion H; tauto.
  - intros; constructor; tauto.
Qed.

Lemma Forall_app_iff :
  forall A (P : A -> Prop) L1 L2, Forall P (L1 ++ L2) <-> Forall P L1 /\ Forall P L2.
Proof.
  intros. induction L1.
  - simpl. firstorder.
  - intros; simpl.
    rewrite !Forall_cons_iff, IHL1. tauto.
Qed.

Lemma Forall_map :
  forall A B (f : A -> B) (P : B -> Prop) L, Forall P (map f L) <-> Forall (fun x => P (f x)) L.
Proof.
  intros. induction L.
  - simpl. firstorder.
  - simpl. rewrite !Forall_cons_iff. firstorder.
Qed.

Lemma Forall_ext_In :
  forall (A : Type) (P1 P2 : A -> Prop) (L : list A), Forall (fun x => P1 x <-> P2 x) L -> Forall P1 L <-> Forall P2 L.
Proof.
  intros. induction L.
  - split; constructor.
  - inversion H; subst.
    rewrite !Forall_cons_iff. tauto.
Qed.

Lemma Forall_True :
  forall (A : Type) (P : A -> Prop) (L : list A), (forall x, P x) -> Forall P L.
Proof.
  intros. induction L.
  - constructor.
  - constructor; auto.
Qed.

Lemma Forall_True_transparent :
  forall (A : Type) (P : A -> Prop) (L : list A), (forall x, P x) -> Forall P L.
Proof.
  intros. induction L.
  - constructor.
  - constructor; auto.
Defined.

Lemma Forall_ext :
  forall (A : Type) (P1 P2 : A -> Prop) (L : list A), (forall x, P1 x <-> P2 x) -> Forall P1 L <-> Forall P2 L.
Proof.
  intros. apply Forall_ext_In.
  apply Forall_True. assumption.
Qed.

Lemma Forall_map_assq :
  forall (A B C : Type) (f : A -> B -> C) (P : A * C -> Prop) (L : list (A * B)), Forall P (map_assq f L) <-> Forall (fun '(x, u) => P (x, f x u)) L.
Proof.
  intros.
  unfold map_assq.
  rewrite Forall_map.
  apply Forall_ext. intros [x u].
  reflexivity.
Qed.

Lemma Forall_filter :
  forall (A : Type) (P : A -> Prop) (f : A -> bool) (L : list A), Forall P (filter f L) <-> Forall (fun x => f x = true -> P x) L.
Proof.
  intros. induction L.
  - simpl. split; constructor.
  - simpl. destruct (f a) eqn:Hfa.
    + rewrite !Forall_cons_iff. tauto.
    + rewrite Forall_cons_iff. intuition congruence.
Qed.

Lemma Forall_filter_eq :
  forall A (P : A -> bool) L, Forall (fun x => P x = true) L -> filter P L = L.
Proof.
  intros A P L. induction L.
  - intros; reflexivity.
  - intros H. simpl. inversion H; subst.
    rewrite H2; simpl; f_equal; apply IHL. assumption.
Qed.

Lemma Forall_In :
  forall (A : Type) (P : A -> Prop) (L : list A), Forall P L <-> (forall x, In x L -> P x).
Proof.
  intros A P L. induction L.
  - simpl. split; intros; [tauto|constructor].
  - rewrite Forall_cons_iff, IHL. simpl.
    firstorder congruence.
Qed.

Lemma Forall_and :
  forall (A : Type) (P Q : A -> Prop) L, Forall P L /\ Forall Q L <-> Forall (fun x => P x /\ Q x) L.
Proof.
  intros A P Q L. induction L as [|x L].
  - simpl. repeat split; constructor.
  - simpl. rewrite !Forall_cons_iff, <- IHL. tauto.
Qed.

Lemma nth_error_Forall_iff :
  forall A (P : A -> Prop) L,
    Forall P L <-> (forall n x, nth_error L n = Some x -> P x).
Proof.
  intros A P L. split.
  - intros H. induction H.
    + intros; destruct n; simpl in *; discriminate.
    + intros [|n]; simpl; [|apply IHForall].
      intros; congruence.
  - induction L as [|x L IH]; intros Hforall; simpl in *.
    + constructor.
    + constructor.
      * apply (Hforall 0); reflexivity.
      * apply IH. intros n; apply (Hforall (S n)).
Qed.

Lemma Forall_impl_transparent :
  forall (A : Type) (P Q : A -> Prop) L, (forall x, P x -> Q x) -> Forall P L -> Forall Q L.
Proof.
  intros A P Q L Himpl H. induction H.
  - constructor.
  - constructor.
    + apply Himpl. assumption.
    + assumption.
Defined.

Lemma Forall_Exists :
  forall (A : Type) (P : A -> Prop) (Q : A -> Prop) (R : Prop) (L : list A),
    (forall x, P x -> Q x -> R) -> Forall P L -> Exists Q L -> R.
Proof.
  intros A P Q R L H1 H2; induction H2; intros H3; inversion H3; subst.
  - eapply H1; eassumption.
  - apply IHForall; assumption.
Qed.

Lemma Forall2_cons_iff :
  forall (A B : Type) (P : A -> B -> Prop) x y L1 L2, Forall2 P (x :: L1) (y :: L2) <-> P x y /\ Forall2 P L1 L2.
Proof.
  intros. split.
  - intros H. inversion H. tauto.
  - intros [H1 H2]. constructor; assumption.
Qed.

Lemma Forall2_map_eq :
  forall (A B C : Type) (f : A -> C) (g : B -> C) L1 L2, map f L1 = map g L2 <-> Forall2 (fun u v => f u = g v) L1 L2.
Proof.
  intros A B C f g L1 L2. split.
  - intros Heq. revert L2 Heq; induction L1 as [|x L1]; intros [|y L2] Heq; simpl in *; try congruence.
    + constructor.
    + injection Heq as Heq1 Heq2. constructor; [assumption|].
      apply IHL1. assumption.
  - intros H. induction H.
    + reflexivity.
    + simpl. f_equal; assumption.
Qed.

Lemma Forall2_map_left :
  forall (A B C : Type) (P : A -> B -> Prop) (f : C -> A) L1 L2, Forall2 P (map f L1) L2 <-> Forall2 (fun u v => P (f u) v) L1 L2.
Proof.
  intros A B C P f L1 L2. revert L2; induction L1 as [|x L1]; intros [|y L2].
  - simpl. split; intros; constructor.
  - simpl. split; intros H; inversion H.
  - simpl. split; intros H; inversion H.
  - simpl. rewrite !Forall2_cons_iff, IHL1. reflexivity.
Qed.

Lemma Forall2_comm :
  forall (A B : Type) (P : A -> B -> Prop) L1 L2, Forall2 P L1 L2 <-> Forall2 (fun u v => P v u) L2 L1.
Proof.
  intros A B P L1 L2. revert L2; induction L1 as [|x L1]; intros [|y L2].
  - simpl. split; intros; constructor.
  - simpl. split; intros H; inversion H.
  - simpl. split; intros H; inversion H.
  - simpl. rewrite !Forall2_cons_iff, IHL1. reflexivity.
Qed.

Lemma Forall2_map_right :
  forall (A B C : Type) (P : A -> B -> Prop) (f : C -> B) L1 L2, Forall2 P L1 (map f L2) <-> Forall2 (fun u v => P u (f v)) L1 L2.
Proof.
  intros A B C P f L1 L2. revert L2; induction L1 as [|x L1]; intros [|y L2].
  - simpl. split; intros; constructor.
  - simpl. split; intros H; inversion H.
  - simpl. split; intros H; inversion H.
  - simpl. rewrite !Forall2_cons_iff, IHL1. reflexivity.
Qed.

Lemma Forall2_map_same :
  forall (A : Type) (P : A -> A -> Prop) L, Forall2 P L L <-> Forall (fun x => P x x) L.
Proof.
  intros A P L. induction L as [|x L].
  - split; constructor.
  - rewrite Forall2_cons_iff, Forall_cons_iff, IHL. reflexivity.
Qed.

Lemma Forall2_impl :
  forall (A B : Type) (P Q : A -> B -> Prop) L1 L2, (forall x y, P x y -> Q x y) -> Forall2 P L1 L2 -> Forall2 Q L1 L2.
Proof.
  intros A B P Q L1 L2 HPQ H. induction H.
  - constructor.
  - constructor; [apply HPQ; assumption|]. assumption.
Qed.

Lemma Forall2_impl_transparent : forall (A B : Type) (P Q : A -> B -> Prop) (L1 : list A) (L2 : list B), (forall (x : A) (y : B), P x y -> Q x y) -> Forall2 P L1 L2 -> Forall2 Q L1 L2.
Proof.
  intros A B P Q L1 L2 Himpl H. induction H.
  - constructor.
  - constructor.
    + apply Himpl. assumption.
    + assumption.
Defined.

Lemma Forall2_In_left :
  forall (A B : Type) (P : A -> B -> Prop) L1 L2 x, Forall2 P L1 L2 -> x \in L1 -> exists y, y \in L2 /\ P x y.
Proof.
  intros A B P L1 L2 x H Hx; induction H; simpl in *.
  - tauto.
  - destruct Hx as [-> | Hx]; [exists y; tauto|].
    destruct (IHForall2 Hx) as (y0 & Hy1 & Hy2); exists y0; tauto.
Qed.

Lemma Forall2_In_right :
  forall (A B : Type) (P : A -> B -> Prop) L1 L2 y, Forall2 P L1 L2 -> y \in L2 -> exists x, x \in L1 /\ P x y.
Proof.
  intros A B P L1 L2 y H Hy; induction H; simpl in *.
  - tauto.
  - destruct Hy as [-> | Hy]; [exists x; tauto|].
    destruct (IHForall2 Hy) as (x0 & Hx1 & Hx2); exists x0; tauto.
Qed.


Lemma Forall2_impl_In_left_transparent :
  forall (A B : Type) (P Q : A -> B -> Prop) L1 L2,
    (forall x y, In x L1 -> P x y -> Q x y) -> Forall2 P L1 L2 -> Forall2 Q L1 L2.
Proof.
  intros A B P Q L1 L2 H Hforall. induction Hforall.
  - constructor.
  - econstructor.
    + apply H; [left; reflexivity|assumption].
    + apply IHHforall.
      intros; eapply H; [right|]; eassumption.
Defined.

Lemma Forall2_In_left_transparent :
  forall (A B : Type) (P : A -> B -> Prop) (Q : Prop) (L1 : list A) (L2 : list B) (x : A) (H : forall y, P x y -> Q), Forall2 P L1 L2 -> x ∈ L1 -> Q.
Proof.
  intros A B P Q L1 L2 x HQ H Hx; induction H.
  - simpl in Hx; tauto.
  - destruct Hx as [-> | Hx]; [eapply HQ; eassumption|apply (IHForall2 Hx)].
Defined.

Lemma Forall2_Exists_left_transparent :
  forall (A B : Type) (P : A -> B -> Prop) (Q : A -> Prop) (R : Prop) (L1 : list A) (L2 : list B) (H : forall x y, P x y -> Q x -> R), Forall2 P L1 L2 -> Exists Q L1 -> R.
Proof.
  intros A B P Q R L1 L2 H HP HQ; induction HP.
  - inversion HQ.
  - inversion HQ; subst; [eapply H; eassumption|].
    apply IHHP, H2.
Defined.


Lemma nth_error_Forall2 :
  forall {A B : Type} {P : A -> B -> Prop} {L1 L2 n x}, Forall2 P L1 L2 -> nth_error L1 n = Some x -> exists y, nth_error L2 n = Some y /\ P x y.
Proof.
  intros A B P. intros L1 L2 n x H; revert n x; induction H; intros n x1 Hx1; destruct n as [|n]; simpl in *; try congruence.
  - injection Hx1; intros; subst. exists y. split; [reflexivity|assumption].
  - apply IHForall2. assumption.
Qed.

Lemma nth_error_Forall2_rev :
  forall {A B : Type} {P : A -> B -> Prop} {L1 L2 n x}, Forall2 P L1 L2 -> nth_error L2 n = Some x -> exists y, nth_error L1 n = Some y /\ P y x.
Proof.
  intros A B P. intros L1 L2 n x H; revert n x; induction H; intros n x1 Hx1; destruct n as [|n]; simpl in *; try congruence.
  - injection Hx1; intros; subst. exists x. split; [reflexivity|assumption].
  - apply IHForall2. assumption.
Qed.

Lemma nth_error_Forall2_None :
  forall {A B : Type} {P : A -> B -> Prop} {L1 L2 n}, Forall2 P L1 L2 -> nth_error L1 n = None <-> nth_error L2 n = None.
Proof.
  intros A B P. intros L1 L2 n H; revert n; induction H; intros n; destruct n as [|n]; simpl in *; try tauto.
  - split; intros; congruence.
  - apply IHForall2.
Qed.

Lemma nth_error_Forall2_iff:
  forall A B (P : A -> B -> Prop) L1 L2,
    Forall2 P L1 L2 <-> (length L1 = length L2 /\ forall n x y, nth_error L1 n = Some x -> nth_error L2 n = Some y -> P x y).
Proof.
  intros A B P L1 L2. split.
  - intros H. induction H.
    + split; [reflexivity|]. intros; destruct n; simpl in *; discriminate.
    + destruct IHForall2 as [Hlen Hforall].
      split; [simpl; congruence|].
      intros [|n]; simpl; [|apply Hforall].
      intros; congruence.
  - revert L2; induction L1 as [|x L1 IH]; intros [|y L2] [Hlen Hforall]; simpl in *.
    + constructor.
    + discriminate.
    + discriminate.
    + constructor; [apply (Hforall 0); reflexivity|].
      apply IH. split; [congruence|].
      intros n; apply (Hforall (S n)).
Qed.

Lemma Forall2_length :
  forall (A B : Type) (P : A -> B -> Prop) L1 L2, Forall2 P L1 L2 -> length L1 = length L2.
Proof.
  intros A B P L1 L2 H. induction H; simpl; congruence.
Qed.

Lemma Forall2_and :
  forall (A B : Type) (P Q : A -> B -> Prop) L1 L2, Forall2 P L1 L2 -> Forall2 Q L1 L2 -> Forall2 (fun x y => P x y /\ Q x y) L1 L2.
Proof.
  intros A B P Q L1 L2 HP. induction HP; intros HQ; inversion HQ; subst.
  - constructor.
  - constructor; [split; assumption|apply IHHP; assumption].
Qed.

Lemma Forall2_select1 :
  forall (A B : Type) (P : A -> Prop) (l1 : list A) (l2 : list B), Forall2 (fun a b => P a) l1 l2 -> Forall P l1.
Proof.
  intros A B P l1 l2 H; induction H; constructor; assumption.
Qed.

Lemma Forall2_select2 :
  forall (A B : Type) (P : B -> Prop) (l1 : list A) (l2 : list B), Forall2 (fun a b => P b) l1 l2 -> Forall P l2.
Proof.
  intros A B P l1 l2 H; induction H; constructor; assumption.
Qed.

Lemma Forall2_and_Forall_left :
  forall (A B : Type) (P : A -> B -> Prop) (Q : A -> Prop) (L1 : list A) (L2 : list B), Forall2 P L1 L2 -> Forall Q L1 -> Forall2 (fun x y => P x y /\ Q x) L1 L2.
Proof.
  intros A B P Q L1 L2 H1; induction H1; intros H2; inversion H2; subst; constructor; tauto.
Qed.

Lemma Forall2_and_Forall_right :
  forall (A B : Type) (P : A -> B -> Prop) (Q : B -> Prop) (L1 : list A) (L2 : list B), Forall2 P L1 L2 -> Forall Q L2 -> Forall2 (fun x y => P x y /\ Q y) L1 L2.
Proof.
  intros A B P Q L1 L2 H1; induction H1; intros H2; inversion H2; subst; constructor; tauto.
Qed.

Lemma Forall2_eq :
  forall (A : Type) (l1 l2 : list A), Forall2 eq l1 l2 -> l1 = l2.
Proof.
  intros A l1 l2 H; induction H.
  - reflexivity.
  - congruence.
Qed.

Lemma Forall2_from_combine :
  forall (A B : Type) (P : A * B -> Prop) l1 l2, length l1 = length l2 -> Forall P (combine l1 l2) -> Forall2 (fun x y => P (x, y)) l1 l2.
Proof.
  intros A B P; induction l1; intros l2; destruct l2; intros H1 Hforall; simpl in *; try congruence.
  - constructor.
  - inversion Hforall; subst. constructor; [assumption|].
    apply IHl1; [congruence|assumption].
Qed.

Lemma Forall_combine_from_Forall2 :
  forall (A B : Type) (P : A * B -> Prop) l1 l2, Forall2 (fun a b => P (a, b)) l1 l2 -> Forall P (combine l1 l2).
Proof.
  intros A B P l1 l2 H; induction H; constructor; assumption.
Qed.

Lemma Forall_square :
  forall (A B C D : Type) (P : A -> B -> Prop) (Q : C -> D -> Prop) (R : A -> C -> Prop) l1 l2 l3 l4,
    Forall2 P l1 l2 -> Forall2 Q l3 l4 -> Forall2 R l1 l3 -> Forall2 (fun b d => exists a c, P a b /\ Q c d /\ R a c) l2 l4.
Proof.
  intros A B C D P Q R; induction l1; intros l2 l3 l4 H1 H2 H3; inversion H1; subst; inversion H3; subst; inversion H2; subst;
    constructor.
  - eexists. eexists. split; [eassumption|]. split; eassumption.
  - eapply IHl1; eassumption.
Qed.

Lemma Exists_neg_Forall2 :
  forall (A B : Type) (P : A -> B -> Prop) l1 l2, Exists (fun xy => ~ P (fst xy) (snd xy)) (combine l1 l2) -> ~ (Forall2 P l1 l2).
Proof.
  intros A B P; induction l1; intros l2 H1 H2; destruct l2; simpl in *; inversion H1; subst; inversion H2; subst; simpl in *.
  - tauto.
  - eapply IHl1; eassumption.
Qed.

Lemma Exists_square :
  forall (A B C D : Type) (P : A -> B -> Prop) (Q : C -> D -> Prop) (R : A * C -> Prop) l1 l2 l3 l4,
    Forall2 P l1 l2 -> Forall2 Q l3 l4 -> Exists R (combine l1 l3) -> Exists (fun bd => exists a c, P a (fst bd) /\ Q c (snd bd) /\ R (a, c)) (combine l2 l4).
Proof.
  intros A B C D P Q R; induction l1; intros l2 l3 l4 H1 H2 H3; inversion H1; subst; simpl in *; inversion H2; subst; simpl in *; inversion H3; subst.
  - apply Exists_cons_hd. eexists. eexists. split; [eassumption|]. split; eassumption.
  - apply Exists_cons_tl. eapply IHl1; eassumption.
Qed.



Inductive Forall3 {A B C : Type} (R : A -> B -> C -> Prop) : list A -> list B -> list C -> Prop :=
| Forall3_nil : Forall3 R nil nil nil
| Forall3_cons : forall x y z l1 l2 l3, R x y z -> Forall3 R l1 l2 l3 -> Forall3 R (x :: l1) (y :: l2) (z :: l3).

Lemma Forall3_impl :
  forall (A B C : Type) (P Q : A -> B -> C -> Prop) l1 l2 l3,
    (forall x y z, P x y z -> Q x y z) -> Forall3 P l1 l2 l3 -> Forall3 Q l1 l2 l3.
Proof.
  intros A B C P Q l1 l2 l3 HPQ H; induction H; constructor; [apply HPQ|]; assumption.
Qed.

Lemma Forall3_app :
  forall (A B C : Type) (P : A -> B -> C -> Prop) l1a l1b l1c l2a l2b l2c, Forall3 P l1a l1b l1c -> Forall3 P l2a l2b l2c -> Forall3 P (l1a ++ l2a) (l1b ++ l2b) (l1c ++ l2c).
Proof.
  intros A B C P l1a l1b l1c l2a l2b l2c H1 H2; induction H1; simpl in *.
  - assumption.
  - constructor; assumption.
Qed.

Lemma Forall3_and :
  forall A B C (P Q : A -> B -> C -> Prop) l1 l2 l3, Forall3 P l1 l2 l3 -> Forall3 Q l1 l2 l3 -> Forall3 (fun a b c => P a b c /\ Q a b c) l1 l2 l3.
Proof.
  intros A B C P Q l1 l2 l3 H1 H2; induction H1; simpl in *; inversion H2; subst; constructor; tauto.
Qed.

Lemma Forall3_select12 :
  forall A B C R (l1 : list A) (l2 : list B) (l3 : list C),
    Forall3 (fun x y z => R x y) l1 l2 l3 -> Forall2 R l1 l2.
Proof.
  intros A B C R l1 l2 l3 H; induction H; constructor; auto.
Qed.

Lemma Forall3_select13 :
  forall A B C R (l1 : list A) (l2 : list B) (l3 : list C),
    Forall3 (fun x y z => R x z) l1 l2 l3 -> Forall2 R l1 l3.
Proof.
  intros A B C R l1 l2 l3 H; induction H; constructor; auto.
Qed.

Lemma Forall3_select23 :
  forall A B C R (l1 : list A) (l2 : list B) (l3 : list C),
    Forall3 (fun x y z => R y z) l1 l2 l3 -> Forall2 R l2 l3.
Proof.
  intros A B C R l1 l2 l3 H; induction H; constructor; auto.
Qed.

Lemma Forall3_select3 :
  forall A B C (P : C -> Prop) (l1 : list A) (l2 : list B) (l3 : list C), Forall3 (fun _ _ c => P c) l1 l2 l3 -> Forall P l3.
Proof.
  intros A B C P l1 l2 l3 H; induction H; simpl in *; constructor; tauto.
Qed.

Lemma Forall3_unselect1 :
  forall A B C (P : A -> Prop) (R : A -> B -> C -> Prop) (l1 : list A) (l2 : list B) (l3 : list C), Forall P l1 -> Forall3 R l1 l2 l3 -> Forall3 (fun a _ _ => P a) l1 l2 l3.
Proof.
  intros A B C P R l1 l2 l3 H1 H2; induction H2; simpl in *; inversion H1; subst; constructor; tauto.
Qed.

Lemma Forall3_unselect2 :
  forall A B C (P : B -> Prop) (R : A -> B -> C -> Prop) (l1 : list A) (l2 : list B) (l3 : list C), Forall P l2 -> Forall3 R l1 l2 l3 -> Forall3 (fun _ b _ => P b) l1 l2 l3.
Proof.
  intros A B C P R l1 l2 l3 H1 H2; induction H2; simpl in *; inversion H1; subst; constructor; tauto.
Qed.

Lemma Forall3_from_Forall2 :
  forall (A B C : Type) (P : A -> B -> Prop) (Q : A -> C -> Prop) l1 l2 l3,
    Forall2 P l1 l2 -> Forall2 Q l1 l3 -> Forall3 (fun x y z => P x y /\ Q x z) l1 l2 l3.
Proof.
  intros A B C P Q l1 l2 l3 H1. revert l3; induction H1; intros l3 H2; inversion H2; subst.
  - constructor.
  - constructor.
    + split; assumption.
    + apply IHForall2. assumption.
Qed.

Lemma Forall3_Exists_2_transparent :
  forall (A B C : Type) (P : A -> B -> C -> Prop) (Q : B -> Prop) (R : Prop) L1 L2 L3 (H : forall x y z, P x y z -> Q y -> R), Forall3 P L1 L2 L3 -> Exists Q L2 -> R.
Proof.
  intros A B C P Q R L1 L2 L3 H HP HQ; induction HP.
  - inversion HQ.
  - inversion HQ; subst; [eapply H; eassumption|].
    apply IHHP, H2.
Defined.

Lemma Forall3_impl_In :
  forall (A B C : Type) (P Q : A -> B -> C -> Prop) L1 L2 L3,
    (forall x y z, In x L1 -> In y L2 -> In z L3 -> P x y z -> Q x y z) -> Forall3 P L1 L2 L3 -> Forall3 Q L1 L2 L3.
Proof.
  intros A B C P Q L1 L2 L3 H Hforall. induction Hforall.
  - constructor.
  - econstructor.
    + apply H; try (left; reflexivity). assumption.
    + apply IHHforall.
      intros; eapply H; try right; assumption.
Qed.

Lemma Forall3_map3 :
  forall (A B C D : Type) (P : A -> B -> D -> Prop) (f : C -> D) (L1 : list A) (L2 : list B) (L3 : list C), Forall3 P L1 L2 (map f L3) <-> Forall3 (fun x y z => P x y (f z)) L1 L2 L3.
Proof.
  intros A B C D P f L1 L2 L3; split; intros H.
  - remember (map f L3) as L4. revert L3 HeqL4.
    induction H; intros; destruct L3; subst; simpl in *; try congruence; constructor.
    + injection HeqL4 as HeqL4; subst. assumption.
    + injection HeqL4 as HeqL4; subst. apply IHForall3. reflexivity.
  - induction H; constructor; assumption.
Qed.

Lemma Forall2_select121 :
  forall (A B : Type) (P : A -> B -> A -> Prop) (L1 : list A) (L2 : list B), Forall2 (fun x y => P x y x) L1 L2 -> Forall3 P L1 L2 L1.
Proof.
  intros A B P L1 L2 H; induction H; constructor; assumption.
Qed.

Lemma Forall2_select12combine :
  forall (A B : Type) (P : A -> B -> A * B -> Prop) (L1 : list A) (L2 : list B), Forall2 (fun x y => P x y (x, y)) L1 L2 -> Forall3 P L1 L2 (combine L1 L2).
Proof.
  intros A B P L1 L2 H; induction H; constructor; assumption.
Qed.

Lemma Forall3_combine23_3 :
  forall (A B C : Type) (P : A -> B -> B * C -> Prop) l1 l2 l3, Forall3 (fun x y z => P x y (y, z)) l1 l2 l3 -> Forall3 P l1 l2 (combine l2 l3).
Proof.
  intros A B C P l1 l2 l3 H; induction H; simpl in *; constructor; assumption.
Qed.

Lemma Forall3_select1 :
  forall (A B C : Type) (P : A -> Prop) l1 (l2 : list B) (l3 : list C), Forall3 (fun x y z => P x) l1 l2 l3 -> Forall P l1.
Proof.
  intros A B C P l1 l2 l3 H; induction H; simpl in *; constructor; assumption.
Qed.


Inductive Forall4 {A B C D : Type} (R : A -> B -> C -> D -> Prop) : list A -> list B -> list C -> list D -> Prop :=
| Forall4_nil : Forall4 R nil nil nil nil
| Forall4_cons : forall x y z w l1 l2 l3 l4, R x y z w -> Forall4 R l1 l2 l3 l4 -> Forall4 R (x :: l1) (y :: l2) (z :: l3) (w :: l4).

Lemma Forall4_impl :
  forall (A B C D : Type) (P Q : A -> B -> C -> D -> Prop) l1 l2 l3 l4,
    (forall x y z w, P x y z w -> Q x y z w) -> Forall4 P l1 l2 l3 l4 -> Forall4 Q l1 l2 l3 l4.
Proof.
  intros A B C D P Q l1 l2 l3 l4 HPQ H; induction H; constructor; [apply HPQ|]; assumption.
Qed.

Lemma Forall4_select123 :
  forall A B C D R (l1 : list A) (l2 : list B) (l3 : list C) (l4 : list D),
    Forall4 (fun x y z w => R x y z) l1 l2 l3 l4 -> Forall3 R l1 l2 l3.
Proof.
  intros A B C D R l1 l2 l3 l4 H; induction H; constructor; auto.
Qed.

Lemma Forall4_select124 :
  forall A B C D R (l1 : list A) (l2 : list B) (l3 : list C) (l4 : list D),
    Forall4 (fun x y z w => R x y w) l1 l2 l3 l4 -> Forall3 R l1 l2 l4.
Proof.
  intros A B C D R l1 l2 l3 l4 H; induction H; constructor; auto.
Qed.

Lemma Forall4_select134 :
  forall A B C D R (l1 : list A) (l2 : list B) (l3 : list C) (l4 : list D),
    Forall4 (fun x y z w => R x z w) l1 l2 l3 l4 -> Forall3 R l1 l3 l4.
Proof.
  intros A B C D R l1 l2 l3 l4 H; induction H; constructor; auto.
Qed.

Lemma Forall4_select234 :
  forall A B C D R (l1 : list A) (l2 : list B) (l3 : list C) (l4 : list D),
    Forall4 (fun x y z w => R y z w) l1 l2 l3 l4 -> Forall3 R l2 l3 l4.
Proof.
  intros A B C D R l1 l2 l3 l4 H; induction H; constructor; auto.
Qed.

Lemma Forall4_select12 :
  forall A B C D R (l1 : list A) (l2 : list B) (l3 : list C) (l4 : list D),
    Forall4 (fun x y z w => R x y) l1 l2 l3 l4 -> Forall2 R l1 l2.
Proof.
  intros A B C D R l1 l2 l3 l4 H; induction H; constructor; auto.
Qed.

Lemma Forall4_select13 :
  forall A B C D R (l1 : list A) (l2 : list B) (l3 : list C) (l4 : list D),
    Forall4 (fun x y z w => R x z) l1 l2 l3 l4 -> Forall2 R l1 l3.
Proof.
  intros A B C D R l1 l2 l3 l4 H; induction H; constructor; auto.
Qed.

Lemma Forall4_select14 :
  forall A B C D R (l1 : list A) (l2 : list B) (l3 : list C) (l4 : list D),
    Forall4 (fun x y z w => R x w) l1 l2 l3 l4 -> Forall2 R l1 l4.
Proof.
  intros A B C D R l1 l2 l3 l4 H; induction H; constructor; auto.
Qed.

Lemma Forall4_select23 :
  forall A B C D R (l1 : list A) (l2 : list B) (l3 : list C) (l4 : list D),
    Forall4 (fun x y z w => R y z) l1 l2 l3 l4 -> Forall2 R l2 l3.
Proof.
  intros A B C D R l1 l2 l3 l4 H; induction H; constructor; auto.
Qed.

Lemma Forall4_select24 :
  forall A B C D R (l1 : list A) (l2 : list B) (l3 : list C) (l4 : list D),
    Forall4 (fun x y z w => R y w) l1 l2 l3 l4 -> Forall2 R l2 l4.
Proof.
  intros A B C D R l1 l2 l3 l4 H; induction H; constructor; auto.
Qed.

Lemma Forall4_select34 :
  forall A B C D R (l1 : list A) (l2 : list B) (l3 : list C) (l4 : list D),
    Forall4 (fun x y z w => R z w) l1 l2 l3 l4 -> Forall2 R l3 l4.
Proof.
  intros A B C D R l1 l2 l3 l4 H; induction H; constructor; auto.
Qed.


Lemma Forall_exists_Forall2 :
  forall (A B : Type) (P : A -> B -> Prop) (l1 : list A),
    Forall (fun x => exists y, P x y) l1 -> exists l2, Forall2 P l1 l2.
Proof.
  intros A B P l1 H; induction H.
  - exists nil. constructor.
  - destruct IHForall as [l2 IH].
    destruct H as [y Hy].
    exists (y :: l2). constructor; assumption.
Qed.

Lemma Forall2_exists_Forall3 :
  forall (A B C : Type) (P : A -> B -> C -> Prop) (l1 : list A) (l2 : list B),
    Forall2 (fun x y => exists z, P x y z) l1 l2 -> exists l3, Forall3 P l1 l2 l3.
Proof.
  intros A B C P l1 l2 H; induction H.
  - exists nil. constructor.
  - destruct IHForall2 as [l3 IH].
    destruct H as [z Hz].
    exists (z :: l3). constructor; assumption.
Qed.

Lemma Forall3_exists_Forall4 :
  forall (A B C D: Type) (P : A -> B -> C -> D -> Prop) (l1 : list A) (l2 : list B) (l3 : list C),
    Forall3 (fun x y z => exists w, P x y z w) l1 l2 l3 -> exists l4, Forall4 P l1 l2 l3 l4.
Proof.
  intros A B C D P l1 l2 l3 H; induction H.
  - exists nil. constructor.
  - destruct IHForall3 as [l4 IH].
    destruct H as [w Hw].
    exists (w :: l4). constructor; assumption.
Qed.

Lemma Forall4_and :
  forall A B C D (P Q : A -> B -> C -> D -> Prop) l1 l2 l3 l4, Forall4 P l1 l2 l3 l4 -> Forall4 Q l1 l2 l3 l4 -> Forall4 (fun a b c d => P a b c d /\ Q a b c d) l1 l2 l3 l4.
Proof.
  intros A B C D P Q l1 l2 l3 l4 H1 H2; induction H1; simpl in *; inversion H2; subst; constructor; tauto.
Qed.

Lemma Forall4_unselect123 :
  forall A B C D (P : A -> B -> C -> Prop) (R : A -> B -> C -> D -> Prop) (l1 : list A) (l2 : list B) (l3 : list C) (l4 : list D), Forall3 P l1 l2 l3 -> Forall4 R l1 l2 l3 l4 -> Forall4 (fun a b c _ => P a b c) l1 l2 l3 l4.
Proof.
  intros A B C D P R l1 l2 l3 l4 H1 H2; induction H2; simpl in *; inversion H1; subst; constructor; tauto.
Qed.




(* Forall using quantifiers *)
Lemma forall_cons_iff :
  forall (A : Type) (P : A -> Prop) a L, (forall x, x \in (a :: L) -> P x) <-> P a /\ (forall x, x \in L -> P x).
Proof.
  intros. simpl. firstorder congruence.
Qed.

Lemma forall_map :
  forall (A B : Type) (P : B -> Prop) (f : A -> B) L, (forall x, x \in map f L -> P x) <-> (forall x, x \in L -> P (f x)).
Proof.
  intros. rewrite <- !Forall_forall. rewrite Forall_map. reflexivity.
Qed.

Lemma forall_pair :
  forall (A B : Type) (P : A -> B -> Prop) L, (forall x y, (x, y) \in L -> P x y) <-> (forall xy, xy \in L -> P (fst xy) (snd xy)).
Proof.
  intros. split; [|firstorder].
  intros H [x y] ?; firstorder.
Qed.

Lemma forall_pair2 :
  forall (A B : Type) (P : A * B -> Prop) L, (forall xy, xy \in L -> P xy) <-> (forall x y, (x, y) \in L -> P (x, y)).
Proof.
  intros. split; [firstorder|]. intros H [x y] ?; firstorder.
Qed.

(* List inclusion and equivalence *)

Definition list_inc {A : Type} (L1 L2 : list A) := forall x, In x L1 -> In x L2.
Definition list_same {A : Type} (L1 L2 : list A) := forall x, In x L1 <-> In x L2.

Notation "L1 '\subseteq' L2" := (list_inc L1 L2) (at level 70, only parsing).
Notation "L1 '⊆' L2" := (list_inc L1 L2) (at level 70).
Notation "L1 '==' L2" := (list_same L1 L2) (at level 70).

Ltac prove_list_inc := (let x := fresh "x" in intros x; simpl; try repeat (rewrite in_app_iff; simpl); tauto).
Ltac prove_list_same := (let x := fresh "x" in intros x; simpl; try repeat (rewrite in_app_iff; simpl); tauto).


Lemma list_inc_trans :
  forall A (L1 L2 L3 : list A), L1 \subseteq L2 -> L2 \subseteq L3 -> L1 \subseteq L3.
Proof.
  intros; unfold list_inc in *; firstorder.
Qed.

Lemma list_inc_app_left :
  forall A (L1 L2 L3 : list A), list_inc (L1 ++ L2) L3 <-> list_inc L1 L3 /\ list_inc L2 L3.
Proof.
  intros; unfold list_inc in *.
  split; [intros H; split; intros x Hx; apply H; rewrite in_app_iff; tauto|].
  intros [H1 H2] x Hx; rewrite in_app_iff in Hx; firstorder.
Qed.

Lemma list_same_inc_iff :
  forall A (L1 L2 : list A), list_same L1 L2 <-> list_inc L1 L2 /\ list_inc L2 L1.
Proof.
  intros; unfold list_same, list_inc. firstorder.
Qed.

Lemma list_same_inc :
  forall A (L1 L2 : list A), list_same L1 L2 -> list_inc L1 L2.
Proof.
  intros. rewrite list_same_inc_iff in H. tauto.
Qed.


Global Instance list_inc_Reflexive {A : Type} : Reflexive (@list_inc A).
Proof.
  firstorder.
Qed.

Global Instance list_inc_Transitive {A : Type} : Transitive (@list_inc A).
Proof.
  firstorder.
Qed.

Global Instance list_inc_PreOrdered {A : Type} : PreOrder (@list_inc A).
Proof.
  split; auto with typeclass_instances.
Qed.

Global Instance list_same_Reflexive {A : Type} : Reflexive (@list_same A).
Proof.
  firstorder.
Qed.

Global Instance list_same_Transitive {A : Type} : Transitive (@list_same A).
Proof.
  firstorder.
Qed.

Global Instance list_same_Symmetric {A : Type} : Symmetric (@list_same A).
Proof.
  firstorder.
Qed.

Global Instance list_same_Equivalence {A : Type} : Equivalence (@list_same A).
Proof.
  split; auto with typeclass_instances.
Qed.

Global Instance app_list_inc_Proper {A : Type} : Proper (list_inc ++> list_inc ++> list_inc) (@app A).
Proof.
  intros L1 L2 H12 L3 L4 H34.
  rewrite list_inc_app_left, H12, H34.
  split; prove_list_inc.
Qed.

Global Instance In_list_inc_Proper {A : Type} : Proper (eq ==> list_inc ++> Basics.impl) (@In A).
Proof.
  intros x1 x2 -> L1 L2 HL.
  firstorder.
Qed.

Global Instance app_list_same_Proper {A : Type} : Proper (list_same ==> list_same ==> list_same) (@app A).
Proof.
  intros L1 L2 H12 L3 L4 H34.
  rewrite list_same_inc_iff in *.
  split; apply app_list_inc_Proper; tauto.
Qed.

Global Instance In_list_same_Proper {A : Type} : Proper (eq ==> list_same ==> iff) (@In A).
Proof.
  intros x1 x2 -> L1 L2 HL.
  apply HL.
Qed.

Global Instance list_inc_list_same_Proper {A : Type} : Proper (list_same ==> list_same ==> iff) (@list_inc A).
Proof.
  intros L1 L2 H12 L3 L4 H34; split; intros H x; specialize (H12 x); specialize (H34 x); specialize (H x); tauto.
Qed.

Lemma one_elem_list_inc :
  forall A (x : A) L, x :: nil \subseteq L <-> x \in L.
Proof.
  intros x L. split.
  - intros H. apply H. simpl. tauto.
  - intros H y Hy. simpl in Hy; destruct Hy as [Hy | []]. subst. assumption.
Qed.

Lemma list_inc_cons_left :
  forall A L1 L2 (x : A), x :: L1 \subseteq L2 <-> x \in L2 /\ L1 \subseteq L2.
Proof.
  intros. rewrite list_inc_app_left with (L1 := x :: nil) (L2 := L1).
  rewrite one_elem_list_inc. reflexivity.
Qed.

Global Instance list_inc_cons_Proper {A : Type} : Proper (eq ==> list_inc ==> list_inc) (@cons A).
Proof.
  intros z1 z2 -> e1 e2 H12 x H. simpl in *. specialize (H12 x). tauto.
Qed.

(* List concatenation *)
Lemma concat_In :
  forall (A : Type) (L : list (list A)) x, In x (concat L) <-> exists l, In x l /\ In l L.
Proof.
  intros A L x. induction L.
  - simpl. firstorder.
  - simpl. rewrite in_app_iff.
    split.
    + intros [H | H]; [|firstorder]. exists a. tauto.
    + intros (l & H1 & [H2 | H2]); [subst; tauto|].
      right. apply IHL. exists l. tauto.
Qed.

Lemma concat_map_In :
  forall (A B : Type) (f : A -> list B) L x, In x (concat (map f L)) <-> exists u, In x (f u) /\ In u L.
Proof.
  intros. rewrite concat_In. split.
  - intros (l & Hx & Hl). rewrite in_map_iff in Hl. destruct Hl as (u & <- & Hu); exists u; split; assumption.
  - intros (u & Hx & Hu). exists (f u). split; [assumption|apply in_map; assumption].
Qed.

Lemma concat_incl :
  forall A (L : list (list A)) L2, concat L \subseteq L2 <-> Forall (fun L3 => L3 \subseteq L2) L.
Proof.
  induction L.
  - intros L2. simpl. split.
    + intros. constructor.
    + intros _ y Hy. simpl in Hy. tauto.
  - intros L2. simpl. rewrite list_inc_app_left. rewrite Forall_cons_iff. f_equiv. apply IHL.
Qed.



(* Induction on length of a list *)
Lemma list_length_ind (A : Type) (P : list A -> Prop) (H0 : P nil) (HS : forall x L, (forall L2, length L = length L2 -> P L2) -> P (x :: L)) : forall L, P L.
Proof.
  intros L. remember (length L) as n. revert L Heqn. induction n.
  - intros L. destruct L.
    + intros; apply H0.
    + simpl; intros; congruence.
  - intros L. destruct L.
    + simpl; intros; congruence.
    + simpl; intros H; injection H; intros; subst. apply HS. apply IHn.
Qed.

(* Smallest integer above all others in a list *)

Fixpoint smallest_above l :=
  match l with
  | nil => 0
  | a :: l => Nat.max (smallest_above l) (S a)
  end.

Lemma smallest_above_gt :
  forall l x, x < smallest_above l <-> exists y, x <= y /\ In y l.
Proof.
  induction l.
  - intros; simpl in *. split; [lia|]. intros (y & Hy1 & Hy2); tauto.
  - intros x. simpl. rewrite Nat.max_lt_iff.
    split.
    + intros [Hx | Hx]; [|exists a; simpl; split; [lia|tauto]].
      apply IHl in Hx. destruct Hx as [y Hy]; exists y; simpl; tauto.
    + intros (y & Hy1 & [Hy2 | Hy2]); [subst; lia|].
      left. apply IHl. exists y. tauto.
Qed.

Lemma smallest_above_map_gt :
  forall {A : Type} (f : A -> nat) l x, x < smallest_above (map f l) <-> exists y, x <= f y /\ In y l.
Proof.
  intros. rewrite smallest_above_gt. split.
  - intros (y & Hy1 & Hy2). rewrite in_map_iff in Hy2. destruct Hy2 as (z & <- & Hz). exists z. tauto.
  - intros (y & Hy1 & Hy2). exists (f y). rewrite in_map_iff. split; [assumption|].
    exists y. tauto.
Qed.

Lemma smallest_above_le :
  forall l x, smallest_above l <= x <-> (forall y, In y l -> y < x).
Proof.
  intros l x. rewrite Nat.le_ngt, smallest_above_gt.
  split; intros H.
  - intros y Hy. rewrite Nat.lt_nge. intros Hy2. apply H. exists y. tauto.
  - intros (y & Hy1 & Hy2). specialize (H y Hy2). lia.
Qed.

Lemma smallest_above_map_le :
  forall {A : Type} (f : A -> nat) l x, smallest_above (map f l) <= x <-> (forall y, In y l -> f y < x).
Proof.
  intros. rewrite smallest_above_le. split.
  - intros H y Hy. apply H. rewrite in_map_iff. exists y; tauto.
  - intros H y Hy. rewrite in_map_iff in Hy. destruct Hy as (z & <- & Hz). apply H. assumption.
Qed.

Lemma smallest_above_app :
  forall L1 L2, smallest_above (L1 ++ L2) = Nat.max (smallest_above L1) (smallest_above L2).
Proof.
  induction L1.
  - intros L2. simpl. reflexivity.
  - intros L2. simpl.
    rewrite IHL1. lia.
Qed.


(* Ordered sublists of a list *)

Inductive sublist_ordered {A : Type} : list A -> list A -> Prop :=
| sublist_ordered_nil : sublist_ordered nil nil
| sublist_ordered_cons_both : forall x L1 L2, sublist_ordered L1 L2 -> sublist_ordered (x :: L1) (x :: L2)
| sublist_ordered_cons_one : forall x L1 L2, sublist_ordered L1 L2 -> sublist_ordered L1 (x :: L2).

Lemma sublist_ordered_map :
  forall (A B : Type) (f : A -> B) L1 L2, sublist_ordered L1 L2 -> sublist_ordered (map f L1) (map f L2).
Proof.
  intros A B f L1 L2 H. induction H.
  - constructor.
  - constructor; assumption.
  - constructor; assumption.
Qed.

Lemma sublist_ordered_map_assq :
  forall (A B C : Type) (f : A -> B -> C) L1 L2, sublist_ordered L1 L2 -> sublist_ordered (map_assq f L1) (map_assq f L2).
Proof.
  intros. apply sublist_ordered_map. assumption.
Qed.

Lemma sublist_ordered_filter :
  forall (A : Type) (P : A -> bool) L, sublist_ordered (filter P L) L.
Proof.
  intros A P L. induction L.
  - constructor.
  - simpl. destruct (P a); constructor; assumption.
Qed.

(* List update *)

Fixpoint update {A : Type} (l : list A) (k : nat) (x : A) : list A :=
  match l with
  | nil => nil
  | y :: l =>
    match k with
    | O => x :: l
    | S k => y :: update l k x
    end
  end.
Arguments update {A} _ _ _ : simpl nomatch.

Lemma nth_error_update :
  forall (A : Type) (l : list A) k x y, nth_error l k = Some x -> nth_error (update l k y) k = Some y.
Proof.
  induction l; intros [|k] x y; simpl in *; intros; try congruence.
  eapply IHl; eassumption.
Qed.

Lemma nth_error_update2 :
  forall (A : Type) (l : list A) k x, nth_error (update l k x) k = match nth_error l k with Some _ => Some x | None => None end.
Proof.
  induction l; intros [|k] x; simpl in *; intros; try congruence.
  apply IHl.
Qed.

Lemma nth_error_update3 :
  forall (A : Type) (l : list A) k1 k2 x, k1 <> k2 -> nth_error (update l k1 x) k2 = nth_error l k2.
Proof.
  induction l; intros [|k1] [|k2] x H; simpl in *; try congruence.
  apply IHl; congruence.
Qed.

Lemma update_length :
  forall {A : Type} (l : list A) k x, length (update l k x) = length l.
Proof.
  induction l; intros [|k] x; simpl in *; congruence.
Qed.

Lemma update_case :
  forall {A : Type} (l : list A) k1 k2 x, (k1 = k2 /\ nth_error (update l k1 x) k2 = Some x) \/ (nth_error (update l k1 x) k2 = nth_error l k2).
Proof.
  intros A l k1 k2 x.
  destruct (Nat.eq_dec k1 k2).
  + subst. rewrite nth_error_update2.
    destruct nth_error; tauto.
  + rewrite nth_error_update3 by assumption. tauto.
Qed.

Lemma nth_error_update_None :
  forall (A : Type) l k1 k2 (x : A), nth_error l k1 = None -> nth_error (update l k2 x) k1 = None.
Proof.
  intros A l; induction l; intros k1 k2 x H; destruct k1; destruct k2; simpl in *; try congruence.
  apply IHl. assumption.
Qed.


Ltac splits n :=
  match n with
  | O => fail
  | S O => idtac
  | S ?n => split; [|splits n]
  end.


Inductive deep_flag := shallow | deep.
Lemma deep_flag_eq_dec : forall (df1 df2 : deep_flag), { df1 = df2 } + { df1 <> df2 }.
Proof.
  intros [|] [|]; solve [left; reflexivity | right; discriminate].
Defined.

Ltac unexistT :=
  repeat match goal with
           [ H : @existT deep_flag _ _ _ = @existT deep_flag _ _ _ |- _ ] =>
           apply inj_pair2_eq_dec in H; [|apply deep_flag_eq_dec]
         end.

Definition option_default {A : Type} (o : option A) (d : A) :=
  match o with Some x => x | None => d end.

Lemma option_map_id : forall (A : Type) (x : option A), option_map id x = x.
Proof.
  intros A [x|]; reflexivity.
Qed.

Definition respectful {A : Type} (R : A -> A -> Prop) (f : A -> A) := forall x y, R x y -> R (f x) (f y).

Fixpoint list_sum l := match l with nil => 0 | x :: l => x + list_sum l end.

Ltac ereplace t :=
  let tmp := fresh "_tmp" in
  let typ := type of t in
  evar (tmp : typ);
  replace t with tmp; unfold tmp.



Lemma and_left :
  forall (A B : Prop), A -> (A -> B) -> A /\ B.
Proof.
  intros A B HA HB; split; [apply HA|apply HB, HA].
Qed.

Lemma and_right :
  forall (A B : Prop), (B -> A) -> B -> A /\ B.
Proof.
  intros A B HA HB; split; [apply HA, HB|apply HB].
Qed.

Ltac and_left := apply and_left.
Ltac and_right := apply and_right.
Tactic Notation "and_left" "as" simple_intropattern(p) := and_left; [|intros p].
Tactic Notation "and_right" "as" simple_intropattern(p) := and_right; [intros p|].

Ltac dedup x :=
  refine ((fun (x : _) => _) _).

Lemma seq_shiftn :
  forall n len a, map (fun k => k + n) (seq a len) = seq (a + n) len.
Proof.
  intros n; induction len; intros a; simpl in *; f_equal.
  apply IHlen.
Qed.

Lemma seq_is_shiftn :
  forall a len, seq a len = map (fun k => k + a) (seq 0 len).
Proof.
  intros a len; rewrite seq_shiftn; reflexivity.
Qed.

Lemma seq_nth_error :
  forall len a n, n < len -> nth_error (seq a len) n = Some (a + n).
Proof.
  induction len; intros a [|n] Hn; simpl in *; try lia.
  - f_equal; lia.
  - rewrite IHlen; [f_equal|]; lia.
Qed.


Lemma NoDup_app :
  forall (A : Type) (l1 l2 : list  A), NoDup l1 -> NoDup l2 -> Forall (fun x => x \notin l2) l1 -> NoDup (l1 ++ l2).
Proof.
  induction l1; intros l2 Hnd1 Hnd2 Hdisj; inversion Hnd1; subst; inversion Hdisj; subst; simpl in *.
  - assumption.
  - constructor.
    + rewrite in_app_iff; tauto.
    + apply IHl1; assumption.
Qed.


Inductive reflect (P : Prop) : bool -> Prop :=
| reflect_true : P -> reflect P true
| reflect_false : ~ P -> reflect P false.

Lemma reflect_iff :
  forall P Q b, P <-> Q -> reflect P b <-> reflect Q b.
Proof.
  intros P Q H; split; intros H1; inversion H1; subst; constructor; tauto.
Qed.

Rewrite.v

Require Import List.
Require Import Arith.
Require Import Misc.
Require Import Psatz.

Definition curry {A B C : Type} (f : A * B -> C) x y := f (x, y).
Definition uncurry {A B C : Type} (f : A -> B -> C) '(x, y) := f x y.
Definition flip {A B C : Type} (f : A -> B -> C) x y := f y x.
Definition union {A B : Type} (R1 R2 : A -> B -> Prop) x y := R1 x y \/ R2 x y.
Definition compose {A B C : Type} (R1 : A -> B -> Prop) (R2 : B -> C -> Prop) x y := exists z, R1 x z /\ R2 z y.

Definition same_rel {A B : Type} (R1 R2 : A -> B -> Prop) :=
  forall x y, R1 x y <-> R2 x y.

Lemma same_rel_refl {A : Type} (R : A -> A -> Prop) : same_rel R R.
Proof.
  intros x y. reflexivity.
Qed.

Lemma same_rel_sym {A B : Type} (R1 R2 : A -> B -> Prop) :
  same_rel R1 R2 -> same_rel R2 R1.
Proof.
  intros H x y; split; intros H1; apply H; assumption.
Qed.

Lemma same_rel_trans {A B : Type} (R1 R2 R3 : A -> B -> Prop) :
  same_rel R1 R2 -> same_rel R2 R3 -> same_rel R1 R3.
Proof.
  intros H1 H2 x y; split; intros H3; [apply H2, H1, H3|apply H1, H2, H3].
Qed.

Lemma flip_flip :
  forall (A B : Type) (R : A -> B -> Prop), same_rel (flip (flip R)) R.
Proof.
  intros A R x y. reflexivity.
Qed.


(* Reflexive closure *)

Definition reflc {A : Type} (R : A -> A -> Prop) x y := R x y \/ x = y.

Lemma same_rel_reflc {A : Type} (R1 R2 : A -> A -> Prop) :
  same_rel R1 R2 -> same_rel (reflc R1) (reflc R2).
Proof.
  intros H x y.
  split; intros [Hxy | ->]; try (right; reflexivity); left; apply H; assumption.
Qed.


(* Symmetric closure *)
Definition symc {A : Type} (R : A -> A -> Prop) := union R (flip R).

Lemma symc_sym {A : Type} (R : A -> A -> Prop) :
  forall x y, symc R x y -> symc R y x.
Proof.
  intros x y [H | H]; [right | left]; assumption.
Qed.


(* Transitive reflexive closure *)

Inductive star {A : Type} (R : A -> A -> Prop) : A -> A -> Prop :=
| star_refl : forall x, star R x x
| star_step : forall x y z, R x y -> star R y z -> star R x z.

Lemma star_1 {A : Type} (R : A -> A -> Prop) :
  forall x y, R x y -> star R x y.
Proof.
  intros x y H. econstructor; [eassumption|].
  constructor.
Qed.

Lemma star_compose :
  forall (A : Type) (R : A -> A -> Prop) x y z, star R x y -> star R y z -> star R x z.
Proof.
  intros A R x y z H. induction H.
  - intros; assumption.
  - intros; econstructor; [eassumption | firstorder].
Qed.

Lemma star_map_impl :
  forall (A B : Type) (RA : A -> A -> Prop) (RB : B -> B -> Prop) (f : A -> B),
    (forall x y, RA x y -> RB (f x) (f y)) -> forall x y, star RA x y -> star RB (f x) (f y).
Proof.
  intros A B RA RB f HR x y H. induction H.
  - constructor.
  - econstructor; eauto.
Qed.

Lemma star_impl :
  forall (A : Type) (R1 R2 : A -> A -> Prop),
    (forall x y, R1 x y -> R2 x y) -> forall x y, star R1 x y -> star R2 x y.
Proof.
  intros A R1 R2 H x y Hxy. eapply star_map_impl with (f := id); eassumption.
Qed.

Lemma same_rel_star {A : Type} (R1 R2 : A -> A -> Prop) :
  same_rel R1 R2 -> same_rel (star R1) (star R2).
Proof.
  intros H x y.
  split; intros Hxy; eapply star_impl; try eassumption; intros; apply H; assumption.
Qed.

Lemma star_preserve :
  forall {A : Type} (R : A -> A -> Prop) (P : A -> Prop), (forall x y, R x y -> P x -> P y) -> forall x y, P x -> star R x y -> P y.
Proof.
  intros A R P H x y Hx Hxy. induction Hxy.
  - assumption.
  - eapply IHHxy, H, Hx. apply H0.
Qed.

Lemma flip_star :
  forall (A : Type) (R : A -> A -> Prop) x y, star (flip R) x y -> star R y x.
Proof.
  intros A R x y H. induction H.
  - apply star_refl.
  - eapply star_compose; [eassumption|]. apply star_1; assumption.
Qed.

Lemma flip_star_iff :
  forall (A : Type) (R : A -> A -> Prop), same_rel (star (flip R)) (flip (star R)).
Proof.
  intros A R x y; split; intros H.
  - apply flip_star. assumption.
  - eapply flip_star, same_rel_star; [|eassumption]. apply flip_flip.
Qed.

Lemma star_star :
  forall (A : Type) (R : A -> A -> Prop), forall x y, star (star R) x y -> star R x y.
Proof.
  intros A R x y H. induction H.
  - constructor.
  - eapply star_compose; eauto.
Qed.

Lemma star_induction_rev :
  forall {A : Type} (R : A -> A -> Prop) (P : A -> Prop) (x : A),
    P x -> (forall y z, P y -> R y z -> P z) -> (forall y, star R x y -> P y).
Proof.
  intros A R P x HPx HPind y Hy. revert HPx.
  induction Hy; firstorder.
Qed.

Lemma star_same :
  forall (A : Type) (R : A -> A -> Prop) t1 t2, t1 = t2 -> star R t1 t2.
Proof.
  intros A R t1 t2 ->. constructor.
Qed.

Lemma star_sym {A : Type} (R : A -> A -> Prop) (Hsym : forall x y, R x y -> R y x) :
  forall x y, star R x y -> star R y x.
Proof.
  intros x y H; induction H.
  - apply star_refl.
  - eapply star_compose; [eassumption|apply star_1, Hsym; assumption].
Qed.

Lemma reflc_star {A : Type} (R : A -> A -> Prop) :
  forall x y, reflc R x y -> star R x y.
Proof.
  intros x y [Hxy | <-]; [apply star_1; assumption|constructor].
Qed.

Lemma star_reflc {A : Type} (R : A -> A -> Prop) :
  same_rel (star R) (star (reflc R)).
Proof.
  intros x y. split; intros H.
  - eapply star_impl; [|eassumption].
    intros; left; assumption.
  - induction H.
    + constructor.
    + destruct H as [H | ->].
      * econstructor; eassumption.
      * assumption.
Qed.

(* Transitive closure *)

Inductive plus {A : Type} (R : A -> A -> Prop) : A -> A -> Prop :=
| plus_1 : forall x y, R x y -> plus R x y
| plus_S : forall x y z, R x y -> plus R y z -> plus R x z.

Lemma plus_map_impl :
  forall (A B : Type) (RA : A -> A -> Prop) (RB : B -> B -> Prop) (f : A -> B),
    (forall x y, RA x y -> RB (f x) (f y)) -> forall x y, plus RA x y -> plus RB (f x) (f y).
Proof.
  intros A B RA RB f HR x y H. induction H.
  - apply plus_1; auto.
  - eapply plus_S; eauto.
Qed.

Lemma plus_impl :
  forall (A : Type) (R1 R2 : A -> A -> Prop),
    (forall x y, R1 x y -> R2 x y) -> forall x y, plus R1 x y -> plus R2 x y.
Proof.
  intros A R1 R2 H x y Hxy. eapply plus_map_impl with (f := id); eassumption.
Qed.

Lemma same_rel_plus :
  forall (A : Type) (R1 R2 : A -> A -> Prop), same_rel R1 R2 -> same_rel (plus R1) (plus R2).
Proof.
  intros A R1 R2 H x y. split; intros Hplus; eapply plus_impl; try eassumption; intros; apply H; assumption.
Qed.

Lemma plus_star :
  forall (A : Type) (R : A -> A -> Prop) x y, plus R x y -> star R x y.
Proof.
  intros A R x y H; induction H.
  - apply star_1. assumption.
  - econstructor; eassumption.
Qed.

Lemma plus_star_iff :
  forall (A : Type) (R : A -> A -> Prop), same_rel (plus R) (compose R (star R)).
Proof.
  intros A R x y; split; intros H.
  - inversion H; subst.
    + exists y; split; [assumption|apply star_refl].
    + exists y0. split; [assumption|apply plus_star; assumption].
  - destruct H as (z & Hxz & Hzy).
    revert x Hxz; induction Hzy; intros w Hw.
    + apply plus_1; assumption.
    + eapply plus_S; [eassumption|apply IHHzy; assumption].
Qed.

Lemma plus_compose_star_left :
  forall (A : Type) (R : A -> A -> Prop) x y z, star R x y -> plus R y z -> plus R x z.
Proof.
  intros A R x y z H1 H2; induction H1; [assumption|].
  econstructor; [eassumption|].
  apply IHstar; assumption.
Qed.

Lemma flip_plus :
  forall (A : Type) (R : A -> A -> Prop) x y, plus (flip R) x y -> plus R y x.
Proof.
  intros A R x y H. induction H.
  - apply plus_1. assumption.
  - eapply plus_compose_star_left; [eapply plus_star; eassumption|].
    apply plus_1. assumption.
Qed.

Lemma flip_plus_iff :
  forall (A : Type) (R : A -> A -> Prop), same_rel (plus (flip R)) (flip (plus R)).
Proof.
  intros A R x y; split; intros H.
  - apply flip_plus. assumption.
  - eapply flip_plus, same_rel_plus; [|eassumption]. apply flip_flip.
Qed.

Lemma plus_compose_star_right :
  forall (A : Type) (R : A -> A -> Prop) x y z, plus R x y -> star R y z -> plus R x z.
Proof.
  intros A R x y z H1 H2.
  apply flip_plus_iff.
  eapply plus_compose_star_left; [|apply flip_plus_iff; eassumption].
  apply flip_star in H2. eassumption.
Qed.


(* Transitive symmetric reflexive closure *)

Definition convertible {A : Type} (R : A -> A -> Prop) := star (symc R).

Lemma convertible_refl {A : Type} (R : A -> A -> Prop) x : convertible R x x.
Proof.
  intros; apply star_refl.
Qed.

Lemma convertible_sym {A : Type} (R : A -> A -> Prop) :
  forall x y, convertible R x y -> convertible R y x.
Proof.
  apply star_sym, symc_sym.
Qed.

Lemma common_reduce_convertible :
  forall (A : Type) (R : A -> A -> Prop) x y z, star R x z -> star R y z -> convertible R x y.
Proof.
  intros A R x y z Hxz Hyz.
  eapply star_compose.
  - eapply star_impl; [|eassumption]. intros; left; assumption.
  - eapply star_impl; [|apply flip_star_iff; eassumption]. intros; right; assumption.
Qed.



(* Confluence *)

Definition commuting_diamond {A : Type} (R1 R2 : A -> A -> Prop) :=
  forall x y z, R1 x y -> R2 x z -> exists w, R2 y w /\ R1 z w.

Definition strongly_commute {A : Type} (R1 R2 : A -> A -> Prop) :=
  forall x y z, R1 x y -> R2 x z -> exists w, reflc R2 y w /\ star R1 z w.

Definition commute {A : Type} (R1 R2 : A -> A -> Prop) := commuting_diamond (star R1) (star R2).

Definition diamond {A : Type} (R : A -> A -> Prop) := commuting_diamond R R.

Definition confluent {A : Type} (R : A -> A -> Prop) := diamond (star R).

Lemma commuting_diamond_symmetric {A : Type} (R1 R2 : A -> A -> Prop) :
  commuting_diamond R1 R2 -> commuting_diamond R2 R1.
Proof.
  intros H x y z H2 H1. destruct (H x z y H1 H2) as (w & Hw2 & Hw1).
  exists w. split; assumption.
Qed.

Lemma commute_symmetric {A : Type} (R1 R2 : A -> A -> Prop) :
  commute R1 R2 -> commute R2 R1.
Proof.
  intros. apply commuting_diamond_symmetric. assumption.
Qed.

Lemma commuting_diamond_ext {A : Type} (R1a R2a R1b R2b : A -> A -> Prop) :
    same_rel R1a R1b -> same_rel R2a R2b -> commuting_diamond R1a R2a <-> commuting_diamond R1b R2b.
Proof.
  intros Heq1 Heq2; split; intros H x y z Hxy Hxz.
  - apply Heq1 in Hxy. apply Heq2 in Hxz. destruct (H _ _ _ Hxy Hxz) as (w & Hyw & Hzw).
    exists w; split; [apply Heq2 | apply Heq1]; assumption.
  - apply Heq1 in Hxy; apply Heq2 in Hxz. destruct (H _ _ _ Hxy Hxz) as (w & Hyw & Hzw).
    exists w; split; [apply Heq2 | apply Heq1]; assumption.
Qed.

Lemma diamond_ext {A : Type} (R1 R2 : A -> A -> Prop) :
  same_rel R1 R2 -> diamond R1 <-> diamond R2.
Proof.
  intros Heq; apply commuting_diamond_ext; assumption.
Qed.

Lemma commute_ext {A : Type} (R1a R2a R1b R2b : A -> A -> Prop) :
  same_rel R1a R1b -> same_rel R2a R2b -> commute R1a R2a <-> commute R1b R2b.
Proof.
  intros Heq1 Heq2. apply commuting_diamond_ext; apply same_rel_star; assumption.
Qed.

Lemma confluent_ext {A : Type} (R1 R2 : A -> A -> Prop) :
  same_rel R1 R2 -> confluent R1 <-> confluent R2.
Proof.
  intros H; apply commute_ext; assumption.
Qed.

Lemma commuting_diamond_strongly_commutes {A : Type} (R1 R2 : A -> A -> Prop) :
  commuting_diamond R1 R2 -> strongly_commute R1 R2.
Proof.
  intros H x y z Hxy Hxz.
  destruct (H x y z Hxy Hxz) as (w & Hw2 & Hw1).
  exists w. split.
  - left. assumption.
  - apply star_1; assumption.
Qed.

Lemma strongly_commute_commutes {A : Type} (R1 R2 : A -> A -> Prop) :
  strongly_commute R1 R2 -> commute R1 R2.
Proof.
  intros H.
  assert (H1 : forall x y z, star R1 x y -> R2 x z -> exists w, reflc R2 y w /\ star R1 z w).
  - intros x y z Hxy; revert z. induction Hxy.
    + intros z Hxz. exists z. split; [left; assumption|constructor].
    + intros w Hw.
      destruct (H _ _ _ H0 Hw) as (t & [Hyt | <-] & Hwt).
      * destruct (IHHxy t Hyt) as (s & Hzs & Hts).
        exists s. split; [assumption|].
        eapply star_compose; eassumption.
      * exists z. split; [right; reflexivity|].
        eapply star_compose; eassumption.
  - intros x y z Hxy Hxz; revert y Hxy. induction Hxz; intros w Hxw.
    + exists w. split; [constructor|assumption].
    + destruct (H1 x w y Hxw H0) as (t & Hwt & Hyt).
      destruct (IHHxz t Hyt) as (s & Hts & Hzs).
      exists s. split; [|assumption].
      eapply star_compose; [|eassumption].
      apply reflc_star; assumption.
Qed.

Lemma commuting_diamond_commutes {A : Type} (R1 R2 : A -> A -> Prop) :
  commuting_diamond R1 R2 -> commute R1 R2.
Proof.
  intros H. apply strongly_commute_commutes, commuting_diamond_strongly_commutes, H.
Qed.

Lemma diamond_is_confluent {A : Type} (R : A -> A -> Prop) :
  diamond R -> confluent R.
Proof.
  apply commuting_diamond_commutes.
Qed.

Lemma between_star {A : Type} (R1 R2 : A -> A -> Prop) :
  (forall x y, R1 x y -> R2 x y) -> (forall x y, R2 x y -> star R1 x y) -> same_rel (star R1) (star R2).
Proof.
  intros H1 H2 x y. split; intros H.
  - eapply star_impl; eassumption.
  - eapply star_star.
    eapply star_impl; eassumption.
Qed.

Definition weak_diamond {A : Type} (R : A -> A -> Prop) :=
  forall x y z, R x y -> R x z -> y = z \/ (exists w, R y w /\ R z w).

Lemma weak_diamond_diamond_reflc {A : Type} (R : A -> A -> Prop) :
  weak_diamond R -> diamond (reflc R).
Proof.
  intros HD x y z [Hxy | <-] [Hxz | <-].
  - specialize (HD x y z Hxy Hxz).
    destruct HD as [-> | (w & Hyw & Hzw)].
    + exists z. split; right; reflexivity.
    + exists w. split; left; assumption.
  - exists y. split; [right; reflexivity|left; assumption].
  - exists z. split; [left; assumption|right; reflexivity].
  - exists x. split; right; reflexivity.
Qed.

Lemma weak_diamond_confluent {A : Type} (R : A -> A -> Prop) :
  weak_diamond R -> confluent R.
Proof.
  intros H.
  apply weak_diamond_diamond_reflc, diamond_is_confluent in H.
  eapply diamond_ext; [|eassumption].
  apply star_reflc.
Qed.


Lemma commuting_confluent :
  forall {A : Type} (R1 R2 : A -> A -> Prop), confluent R1 -> confluent R2 -> commute R1 R2 -> confluent (union R1 R2).
Proof.
  intros A R1 R2 Hcf1 Hcf2 Hcomm.
  assert (H : diamond (compose (star R1) (star R2))).
  - intros x1 z1 x3 (y1 & Hxy1 & Hyz1) (x2 & Hx12 & Hx23).
    destruct (Hcf1 _ _ _ Hxy1 Hx12) as (y2 & Hy12 & Hxy2).
    destruct (Hcomm _ _ _ Hy12 Hyz1) as (z2 & Hyz2 & Hz12).
    destruct (Hcomm _ _ _ Hxy2 Hx23) as (y3 & Hy23 & Hxy3).
    destruct (Hcf2 _ _ _ Hy23 Hyz2) as (z3 & Hyz3 & Hz23).
    exists z3.
    split; [exists z2|exists y3]; split; assumption.
  - apply diamond_is_confluent in H.
    eapply diamond_ext; [|exact H]. apply between_star.
    + intros x y [H1 | H2]; [exists y|exists x]; split; econstructor; try eassumption; constructor.
    + intros x z (y & Hxy & Hyz).
      eapply star_compose; eapply star_impl; try eassumption;
        intros u v Huv; [left|right]; assumption.
Qed.


Lemma convertible_confluent_common_reduce :
  forall (A : Type) (R : A -> A -> Prop),
    confluent R -> forall x y, convertible R x y -> exists z, star R x z /\ star R y z.
Proof.
  intros A R Hconf x y Hconv. induction Hconv.
  - exists x. split; constructor.
  - destruct IHHconv as (w & Hyw & Hzw).
    destruct H as [Hxy | Hyx].
    + exists w. split; [|assumption]. econstructor; eassumption.
    + destruct (Hconf y x w) as (t & Hxt & Hwt).
      * apply star_1. assumption.
      * assumption.
      * exists t. split; [assumption|].
        eapply star_compose; eassumption.
Qed.


(* Rewriting one element of a list *)

Inductive step_one {A : Type} (R : A -> A -> Prop) : list A -> list A -> Prop :=
| step_one_step : forall x y L, R x y -> step_one R (x :: L) (y :: L)
| step_one_cons : forall x L1 L2, step_one R L1 L2 -> step_one R (x :: L1) (x :: L2).

Lemma step_one_decompose :
  forall (A : Type) (R : A -> A -> Prop) l1 l2, step_one R l1 l2 <-> exists l3 l4 x y, l1 = l3 ++ x :: l4 /\ l2 = l3 ++ y :: l4 /\ R x y.
Proof.
  intros A R l1 l2. split; intros H.
  - induction H.
    + exists nil, L, x, y. tauto.
    + destruct IHstep_one as (l3 & l4 & a & b & H1); exists (x :: l3), l4, a, b.
      simpl; intuition congruence.
  - destruct H as (l3 & l4 & x & y & -> & -> & H).
    induction l3; simpl; constructor; assumption.
Qed.

Lemma step_one_star :
  forall (A : Type) (R : A -> A -> Prop), same_rel (star (step_one R)) (Forall2 (star R)).
Proof.
  intros A R x y. split; intros H.
  - induction H.
    + apply Forall2_map_same, Forall_True. intros; apply star_refl.
    + enough (Forall2 (star R) x y).
      * apply Forall2_comm in H1.
        eapply Forall3_select23, Forall3_impl; [|eapply Forall3_from_Forall2; eassumption].
        intros ? ? ? [? ?]; eapply star_compose; simpl in *; eassumption.
      * clear H0 IHstar. induction H; constructor.
        -- apply star_1; assumption.
        -- apply Forall2_map_same, Forall_True. intros; apply star_refl.
        -- apply star_refl.
        -- assumption.
  - induction H.
    + apply star_refl.
    + eapply star_compose; [|eapply star_map_impl with (f := fun l => y :: l); [|eassumption]; intros; constructor; assumption].
      eapply star_map_impl with (f := fun x => x :: l); [|eassumption].
      intros; constructor; assumption.
Qed.

Lemma step_one_impl_transparent :
  forall (A : Type) (R1 R2 : A  -> A -> Prop) L1 L2, (forall x y, R1 x y -> R2 x y) -> step_one R1 L1 L2 -> step_one R2 L1 L2.
Proof.
  intros A R1 R2 L1 L2 H1 H2; induction H2; constructor; [|assumption].
  apply H1, H.
Defined.

Lemma step_one_impl_strong_transparent :
  forall (A : Type) (R1 R2 : A -> A -> Prop) L1 L2, (forall x y, R1 x y -> R2 x y) -> step_one R1 L1 L2 -> step_one (fun x y => R1 x y /\ R2 x y) L1 L2.
Proof.
  intros A R1 R2 L1 L2 H1 H2. eapply step_one_impl_transparent; [|eassumption].
  intros; split; [assumption|apply H1; assumption].
Defined.


Lemma star_list :
  forall (A B : Type) (RA : A -> A -> Prop) (RB : B -> B -> Prop) (f : list A -> B) l1 l2,
    (forall l1 l2 x y, RA x y -> RB (f (l1 ++ x :: l2)) (f (l1 ++ y :: l2))) -> Forall2 (star RA) l1 l2 -> star RB (f l1) (f l2).
Proof.
  intros A B RA RB f l1 l2 Himpl Hl.
  enough (H : forall l, star RB (f (l ++ l1)) (f (l ++ l2))); [exact (H nil)|].
  induction Hl as [|x y l1 l2 Hxy Hl IH].
  - intros. constructor.
  - intros l. eapply star_compose.
    + specialize (IH (l ++ x :: nil)). rewrite <- !app_assoc in IH. apply IH.
    + eapply star_map_impl with (f := fun t => f (l ++ t :: l2)); [|eassumption].
      intros; apply Himpl; assumption.
Qed.


Lemma Acc_star_down :
  forall (A : Type) (R : A -> A -> Prop) x y, Acc R x -> star R y x -> Acc R y.
Proof.
  intros A R x y H1 H2. induction H2.
  - assumption.
  - apply IHstar in H1. inversion H1.
    apply H0. assumption.
Qed.


Lemma Acc_plus :
  forall (A : Type) (R : A -> A -> Prop) x, Acc R x -> Acc (plus R) x.
Proof.
  intros A R x H. induction H.
  constructor. intros y Hy.
  apply flip_plus_iff in Hy.
  inversion Hy; subst.
  - apply H0. assumption.
  - eapply Acc_star_down; [eapply H0; eassumption|].
    apply star_1, flip_plus_iff; eassumption.
Qed.


Definition updatep {A B : Type} (f : A -> B -> Prop) (x : A) (P : B -> Prop) (u : A) (v : B) :=
  (u <> x /\ f u v) \/ (u = x /\ P v).

Inductive AccI {A : Type} (B : A -> Prop) (R : A -> A -> Prop) : A -> Prop :=
| AccI_base : forall a, B a -> AccI B R a
| AccI_intro : forall a, (forall b, R b a -> AccI B R b) -> AccI B R a.

Lemma updatep_wf2 :
  forall (A : Type) (R : A -> A -> Prop) u (P : A -> Prop),
    (forall v, P v -> AccI (fun v => plus R u v) (flip (updatep R u P)) v) -> well_founded (flip R) -> well_founded (flip (updatep R u P)).
Proof.
  intros A R u P H Hwf v.
  induction (Acc_plus _ _ _ (Hwf v)). constructor.
  intros v [[Huv HR] | [-> HP]].
  - apply H1, plus_1, HR.
  - specialize (H _ HP). clear HP. induction H.
    + apply H1, flip_plus_iff, H.
    + constructor. apply H2.
Qed.

Lemma updatep_wf_none :
  forall (A : Type) (R : A -> A -> Prop) u (P : A -> Prop),
    ~ P u -> (forall v, ~ R v u) -> well_founded (flip R) -> well_founded (flip (updatep R u P)).
Proof.
  intros A R u P HP Hu Hwf.
  assert (Hwf1 : forall v, v <> u -> Acc (flip (updatep R u P)) v).
  - intros v Hv. induction (Hwf v). constructor.
    intros v [[Huv HR] | [-> HPv]].
    + apply H0; [assumption|]. intros ->; eapply Hu, HR.
    + tauto.
  - intros v. constructor; intros w [[Hvw HR2] | [-> HPw]].
    + apply Hwf1. intros ->; eapply Hu, HR2.
    + apply Hwf1. intros ->; apply HP, HPw.
Qed.

Lemma Acc_ext :
  forall (A : Type) (R1 R2 : A -> A -> Prop) x, (forall u v, R2 u v -> R1 u v) -> Acc R1 x -> Acc R2 x.
Proof.
  intros A R1 R2 x H Hwf; induction Hwf; constructor.
  intros y HR; apply H1, H, HR.
Qed.

Lemma AccI_ext :
  forall (A : Type) (B : A -> Prop) (R1 R2 : A -> A -> Prop) x, (forall u v, R2 u v -> R1 u v) -> AccI B R1 x -> AccI B R2 x.
Proof.
  intros A B R1 R2 x H Hwf; induction Hwf.
  - apply AccI_base; assumption.
  - apply AccI_intro; intros; apply H1, H, H2.
Qed.

Lemma well_founded_ext :
  forall (A : Type) (R1 R2 : A -> A -> Prop), (forall u v, R2 u v -> R1 u v) -> well_founded R1 -> well_founded R2.
Proof.
  intros A R1 R2 H Hwf x; eapply Acc_ext; [eassumption|apply Hwf].
Qed.

Lemma Acc_cycle :
  forall (A : Type) (R : A -> A -> Prop) x, plus R x x -> Acc (flip R) x -> False.
Proof.
  intros A R x Hplus Hacc. induction Hacc.
  inversion Hplus; subst.
  - eapply H0; eassumption.
  - eapply H0; [eassumption|].
    eapply plus_compose_star_right; [eassumption|].
    apply star_1; assumption.
Qed.