Append and Split is same as doing nothing

Question

I want to prove following lemmas.

Lemma AppendAndSplit {n m}(e:Euc n) (f:Euc m): # (e +++ f) = (e, f).
Proof.
induction e.
reflexivity.
remember (r:::e).
Admitted.

Lemma SplitRule {n m}(e:Euc (n+m)) : (fst (# e)) +++ (snd (# e)) = e.
Proof.
induction n.
reflexivity.
Admitted.

# and +++ are notations of EucAppend and Split_Euc. I can feel that these hold, but I don't know how prove them.

Please tell me some techniques.

(* There are codes needed below *)

Require Import Coq.Reals.Reals.

Inductive Euc:nat -> Type:=
|RO : Euc 0
|Rn : forall {n:nat}, R -> Euc n -> Euc (S n).

Notation "[ ]" := RO.
Notation "[ r1 , .. , r2 ]" := (Rn r1 .. ( Rn r2 RO ) .. ).
Infix ":::" := Rn (at level 60, right associativity).

Fixpoint EucAppend {n m} (e:Euc n) (f:Euc m) :Euc (n+m):=
 match e with
 |[] => f
 |e' ::: es => e' ::: (EucAppend es f)
 end.

Infix "+++" := EucAppend (at level 60, right associativity).

Fixpoint split_Euc {n m : nat} (xi : Euc (n + m)) : Euc n ∧ Euc m.
Proof.
  destruct n as [ | n].
  - exact (RO, xi).
  - inversion_clear xi.
    apply split_Euc in H0  as [l r].
    exact (Rn H l, r).
Defined.

Notation "# n" := (split_Euc n) (at level 60, right associativity).

Answer 1

The main problem you cannot solve your goals is because of the definitional problem. Split_Euc is defined to perform induction on n, and that's okay however, the definitions perform an inversion on Euc. Inversion is normally a tactic for proofs, once the tactics generate very heavy proofs terms :

Fixpoint split_Euc {n m : nat} (xi : Euc (n + m)) : Euc n * Euc m.
Proof.
  destruct n as [ | n].
  - exact (RO, xi).
  - inversion_clear xi.
    Show Proof. (* let see what is actually the problem *)
    ...
Defined.

You'll see something like that :

       eq_rec_r (fun n2 : nat => R -> Euc n2 -> Euc (S n0) * Euc m)
         (fun (H6 : R) (H7 : Euc (n0 + m)) =>
          ?Goal@{n:=n0; H:=H6; H0:=H7}) H5) H3) H1 H H0

Notice your definition uses a proof (induction scheme of equality) term to make the join of the tuple. Proofs terms are not easily normalized and some others don't even get a normalized term (it is the case of Opaque proofs). The solution is to avoid tactics that generate heavy proofs terms and substitute for inductions schemes (like destruct, induction, case...), once they are "free" or almostt of automatic proofs.

Definition rect_euc {n : nat} (v : Euc (S n)) : forall (P : Euc (S n) -> Type) (H : forall ys a, P (a ::: ys)), P v.
  refine (
    match v  with
       |@Rn _ _ _ => _
       |R0 => _
    end).
   exact idProp.
  intros.
  apply : H.
Defined.

Fixpoint split_Euc {n m : nat} (xi : Euc (n + m)) : Euc n * Euc m.
Proof.
  destruct n as [ | n].
  - exact (RO, xi).
  - elim/@rect_euc : xi.
    intros.
   pose (split_Euc _ _ ys).
   exact (Rn a (fst p), (snd p)).
Defined.

Now, as split_euc is defined using induction on n, you should do the same to get a straightforward proof.

Lemma AppendAndSplit {n m}(e:Euc n) (f:Euc m): # (e +++ f) = (e, f).
Proof.
  induction n.
  - remember 0.
    destruct e.
    reflexivity.
    inversion Heqn.
  - apply (rect_euc e).
    intros.
    assert (forall n (xs ys : Euc n) (x y : R), x = y -> xs = ys -> x ::: xs = y ::: ys).
      intros.
      rewrite H; rewrite H0; trivial.
    pose (IHn ys).
    apply : injective_projections.
    simpl;apply : H; trivial.
    exact (f_equal fst e0).
    exact (f_equal snd e0).
Qed.

Lemma SplitRule {n m}(e:Euc (n+m)) : (fst (split_Euc e)) +++ (snd (split_Euc e)) = e.
  YOUR_TURN. (* now it's your turn, just do the same and u will get the goal*)
Qed.