alternate_refine.v

Require Import List.
Require Import Sorting.Permutation.
Require Import Arith.
Require Import Wf_nat.
Require Import ssreflect.

Section Alternate.

Variable A : Type.

Record lr := mk_lr {
  fls : list A;
  sls : list A
}.

Definition lrlt (r r' : lr) : Prop := 
  length (fls r ++ sls r) < length (fls r' ++ sls r').

Theorem lrlt_well_founded : well_founded lrlt.
Proof.
 apply well_founded_lt_compat with (f := fun r => length (fls r ++ sls r)).
 by move => x y; rewrite /lrlt => H.
Defined.

Inductive alternation : list A -> list A -> list A -> Prop :=
| alt_nil : forall l, alternation nil l l
| alt_step : forall a, forall l t t', alternation l t t' -> alternation (a::t) l (a::t').

Definition alternate_t (r : lr) : Type :=   
  { l : list A | alternation (fls r) (sls r) l }.

Definition alternate_F : forall r : lr, (forall r' : lr, lrlt r' r -> alternate_t r') -> alternate_t r.
rewrite /alternate_t.
refine
  (fun (r : lr) alternate_rec => 
    match (fls r) as l return (fls r = l -> alternate_t r) with
    | nil => fun (H_eq : fls r = nil) =>
      exist _ (sls r) _
    | a :: l0 => fun (H_eq : fls r = a :: l0) => 
      match alternate_rec (mk_lr (sls r) l0) _ with
      | exist _ l' H_ex => 
        exist _ (a :: l') _
      end
    end (refl_equal (fls r))).
- by rewrite H_eq; apply alt_nil.
- rewrite /lrlt H_eq /=.
  have H_perm: Permutation (l0 ++ sls r) (sls r ++ l0) by apply: Permutation_app_swap.
  have ->: length (l0 ++ sls r) = length (sls r ++ l0) by apply: Permutation_length H_perm.
  exact: lt_n_Sn.
- by rewrite H_eq; apply: alt_step H_ex.
Defined.
  
Definition alternate : forall (r : lr), alternate_t r :=
 @well_founded_induction_type
  lr
  lrlt
  lrlt_well_founded
  alternate_t
  alternate_F.

End Alternate.