The Coq mailing list

[mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>]

Hi everyone,

How can I prove the theorem, go_app, shown below? I find it slightly
amusing that in the base there is not enough information that I can
use to discharge it.  You can see the complete source code [1] (I
manage to prove this theorem for a simplified definition of go using
filter [2])

 Fixpoint go (z : A) (xs : list A) : list A * list A :=
    match xs with
    | [] => ([], [])
    | (x :: xs) =>
      match go z xs with
      | (ys, zs) =>
        match R x z with
        | true => (x :: ys, zs)
        | _ => (ys, x :: zs)
        end
      end
    end.


Theorem go_app :
    ∀ (xs ys zs : list A) (z : A),
    In z xs ->
    (ys, zs) = go z xs -> Permutation (ys ++ zs) xs.
  Proof.
    refine(fix Fn xs {struct xs} :=
      match xs as xsp return xs = xsp -> _
      with
      | [] => fun Ha => _
      | xh :: xst => fun Ha => _
      end eq_refl);
      simpl;
      intros ? ? ? Hb Hc.
    +
      refine(match Hb with end).
    +
      refine(match Hb with
        | or_introl Hap => _
        | or_intror Hap => _
        end).
      ++
        rewrite Hap in Hc.
        rewrite R_refl in Hc.
        (* There is no information in the context that
          connects xst to xsh and ysh *)
        destruct (go z xst) as (xsh, ysh) eqn:He.
        inversion Hc; subst; clear Hc; simpl.
        constructor.
        (* Now I am stuck! Because this is what
          I am trying to discharge so I am chasing my tail?
        *)
        admit.
      ++
        destruct (R xh z) eqn:Hd.
        +++
          destruct (go z xst) as (xsh, ysh) eqn:He.
          inversion Hc; subst; clear Hc; simpl.
          constructor.
          eapply Fn;
          [exact Hap | eapply eq_sym; exact He].
        +++
          destruct (go z xst) as (xsh, ysh) eqn:He.
          inversion Hc; subst; clear Hc; simpl.
          eapply Permutation_sym, Permutation_cons_app,
            Permutation_sym.
          eapply Fn;
          [exact Hap | eapply eq_sym; exact He].
    Admitted.


Best,
Mukesh

[1] https://gist.github.com/mukeshtiwari/55439c129b35071585e05c9847a96c59
[2] 
https://gist.github.com/mukeshtiwari/55439c129b35071585e05c9847a96c59#file-constant_space-v-L17