Extraction.v

From Stdlib Require Import 
  Vector Fin Bool Utf8
  Psatz BinIntDef.
Import VectorNotations EqNotations. 


Notation "'existsT' x .. y , p" :=
  (sigT (fun x => .. (sigT (fun y => p)) ..))
    (at level 200, x binder, right associativity,
     format "'[' 'existsT' '/ ' x .. y , '/ ' p ']'") : type_scope.


Section Ins.
  Context {R : Type}.


  Lemma vector_inv_S : 
      forall {n : nat} (v : Vector.t R (S n)), {h & {t & v = h :: t}}.
  Proof.
    intros n v.
    refine 
      (match v as v' in Vector.t _ n' return
        (match n' return Vector.t R n' -> Type  
        with 
        | 0 => fun _ => IDProp
        | S n'' => fun (ea : Vector.t R (S n'')) => 
          {h : R & {t : Vector.t R n'' & ea = h :: t}}
        end v')
      with
      | cons _ h _ t => existT _ h (existT _ t eq_refl)
      end).
  Defined.


  Lemma fin_inv_S (n : nat) (i : Fin.t (S n)) :
    (i = Fin.F1) + {i' | i = Fin.FS i'}.
  Proof.
    refine (match i with
            | Fin.F1 => _
            | Fin.FS _ => _
            end); eauto.
  Defined.


  Definition take : forall (n : nat) {m : nat}, 
    Vector.t R (n + m) -> Vector.t R n.
  Proof.
    refine(
      fix Fn n {struct n} :=
      match n with 
      | 0 => fun _ _ => []
      | S n' => fun _ v => _
      end).
    cbn in v.
    destruct (vector_inv_S v) as (vh & vtl & _).
    exact (vh :: Fn _ _ vtl).
  Defined.


  Definition drop : forall (n : nat) {m : nat}, 
    Vector.t R (n + m) -> Vector.t R m.
  Proof.
    refine(
      fix Fn n {struct n} :=
      match n with 
      | 0 => fun _ v => v
      | S n' => fun _ v => _
      end).
    cbn in v.
    destruct (vector_inv_S v) as (_ & vtl & _).
    exact (Fn _ _ vtl).
  Defined.

Theorem take_drop_inv : ∀ (n m : nat) (v : Vector.t R (n + m)),
    v = take n v ++ drop n v.
  Proof.
    induction n as [|n ihn].
    +
      cbn; intros *.
      reflexivity.
    +
      cbn; intros *.
      destruct (vector_inv_S v) as (vh & vt & ha).
      cbn. rewrite ha. f_equal.
      erewrite <-ihn.
      reflexivity.
  Qed.

  Theorem rew_eq_refl : ∀ (n m : nat) (v₁ : Vector.t R n)
    (v₂ : Vector.t R m) (vh : R) (pf : n = m), 
    v₁ = rew <-pf in v₂ -> 
    vh :: v₁ = rew <- [Vector.t R] f_equal S pf in (vh :: v₂).
  Proof.
    intros * ha.
    subst; cbn; reflexivity.
  Qed.
  
  Theorem vector_fin_app : ∀ (n : nat) (f : Fin.t n) (v : Vector.t R n),
     existsT (m₁ m₂ : nat) (v₁ : Vector.t R m₁) (vm : R) 
      (v₂ : Vector.t R m₂)
      (pf : n = m₁ + (1 + m₂)), 
      v = rew  <- [Vector.t R] pf in (v₁ ++ [vm] ++ v₂) ∧
      vm = Vector.nth v f ∧
      m₁ = proj1_sig  (Fin.to_nat f).
  Proof.
    induction n as [|n ihn].
    +
      intros *.
      refine match f with end.
    +
      intros *.
      destruct (fin_inv_S _ f) as [f' | (f' & ha)].
      ++
        subst; cbn.
        destruct (vector_inv_S v) as (vh & vt & hb).
        exists 0, n, [], vh, vt, eq_refl. 
        subst; cbn.
        repeat split; reflexivity.
      ++
        (* inductive case *)
        destruct (vector_inv_S v) as (vh & vt & hb).
        subst; cbn.
        destruct (ihn f' vt) as (m₁ & m₂ & v₁ & vm & v₂ & pf & ha & hb & hc).
        exists (S m₁), m₂, (vh :: v₁), vm, v₂, (f_equal S pf).
        cbn; split.
        eapply rew_eq_refl; exact ha.
        split. 
        exact hb.
        destruct (to_nat f') as (u & hu).
        cbn in hc |- *.
        subst. reflexivity.
  Defined.

  
  
  Theorem vector_fin_app_pred : ∀ (n : nat) (f : Fin.t (1 + n))
    (va : Vector.t R (1 + n)) (vb : Vector.t R n),
    existsT (m₁ m₂ : nat) (v₁ v₃ : Vector.t R m₁) (vm : R)
      (v₂ v₄ : Vector.t R m₂)
      (pfa : (1 + n = (m₁ + (1 + m₂)))) (pfb : (n = m₁ + m₂)),
      (va = rew  <- [Vector.t R] (pfa) in ((v₁ ++ [vm] ++ v₂)) ∧
      vm = Vector.nth va f ∧
      vb = rew  <- [Vector.t R] (pfb) in ((v₃ ++ v₄)) ∧
      m₁ = proj1_sig  (Fin.to_nat f)).
  Proof.
    intros *.
    destruct (vector_fin_app _ f va) as 
    (m₁ & m₂ & v₁ & vm & v₂ & pf & ha & hb).
    assert (hc : n = m₁ + m₂) by nia. subst.
    exists m₁, m₂, v₁, (take m₁ vb), 
    vm, v₂, (drop m₁ vb), pf, eq_refl. 
    subst; cbn in * |- *.
    split. reflexivity.
    destruct hb as (hb & hc).
    split. exact hb.
    split. 
    eapply take_drop_inv.
    destruct (to_nat f) as (u & hu).
    cbn in hc |- *.
    subst. reflexivity.
  Defined.


  Record Box (P : Prop) : Type := { p : P }.
  Arguments p {_} _.
  
  Theorem vector_fin_app_pred_box : ∀ (n : nat) (f : Fin.t (1 + n))
    (va : Vector.t R (1 + n)) (vb : Vector.t R n),
    existsT (m₁ m₂ : nat) (v₁ v₃ : Vector.t R m₁) (vm : R)
      (v₂ v₄ : Vector.t R m₂)
      (pfa : Box (1 + n = (m₁ + (1 + m₂)))) (pfb : Box (n = m₁ + m₂)),
      Box (va = rew  <- [Vector.t R] (p pfa) in ((v₁ ++ [vm] ++ v₂)) ∧
      vm = Vector.nth va f ∧
      vb = rew  <- [Vector.t R] (p pfb) in ((v₃ ++ v₄)) ∧
      m₁ = proj1_sig  (Fin.to_nat f)).
  Proof.
    intros *.
    destruct (vector_fin_app _ f va) as
    (m₁ & m₂ & v₁ & vm & v₂ & pf & ha & hb).
    assert (hc : n = m₁ + m₂) by nia. subst.
    exists m₁, m₂, v₁, (take m₁ vb),
    vm, v₂, (drop m₁ vb), (Build_Box _ pf), (Build_Box _ eq_refl).
    subst; cbn in * |- *.
    split. split. reflexivity.
    destruct hb as (hb & hc).
    split. exact hb.
    split.
    eapply take_drop_inv.
    destruct (to_nat f) as (u & hu).
    cbn in hc |- *.
    subst. reflexivity.
  Defined.
End Ins.

From Stdlib Require Import Extraction.
Extraction Language Haskell.
Recursive Extraction vector_fin_app_pred_box.