Encode-decode for the polynomials

poly.v

Fixpoint code_poly (P Q : polynomial) : Type := 
  match P, Q with
  | poly_var, poly_var => Unit
  | poly_const C, poly_const C' => C = C'
  | poly_times Q R, poly_times Q' R' => (code_poly Q Q') * (code_poly R R')
  | poly_plus Q R , poly_plus Q' R'  => (code_poly Q Q') * (code_poly R R')
  | _, _ => Empty
  end.


Fixpoint encode_refl P : code_poly P P.
Proof. 
  destruct P; simpl; try reflexivity.
  - refine (encode_refl P1, encode_refl P2).
  - refine (encode_refl P1, encode_refl P2).
Defined.

Definition encode (P Q : polynomial) (p : P = Q) : code_poly P Q :=
  p # encode_refl P.

Lemma decode (P Q : polynomial) : code_poly P Q -> P = Q.
Proof.
  revert Q. induction P, Q; simpl;
  intros H; try (refine (Empty_rec H) || reflexivity).
  - refine (ap _ H).
  - destruct H as [H H'].
    refine (ap (poly_times _) _ @ _).
    apply IHP2. apply H'.
    refine (ap (fun z => poly_times z _) _).
    by apply IHP1.
  - destruct H as [H H'].
    refine (ap (poly_plus _) _ @ _).
    apply IHP2. apply H'.
    refine (ap (fun z => poly_plus z _) _).
    by apply IHP1.
Defined.

Lemma decode_encode (P Q : polynomial) (p : P = Q) :
  decode _ _ (encode _ _ p) = p.
Proof.
  destruct p; simpl.
  induction P; simpl; try reflexivity.
  - rewrite IHP1, IHP2. hott_simpl.
  - rewrite IHP1, IHP2. hott_simpl.
Defined.

Lemma encode_decode (P Q : polynomial) (c : code_poly P Q) :
  encode _ _ (decode _ _ c) = c.
Proof.
  revert Q c. induction P, Q; simpl; intros c; try refine (Empty_rec c).
  - destruct c. reflexivity.
  - destruct c. reflexivity.
  - destruct c as [c c'].
    specialize (IHP1 _ c).
    specialize (IHP2 _ c').
    destruct (decode P2 Q2 c').
    destruct (decode P1 Q1 c).
    simpl.
    rewrite <- IHP1.
    rewrite <- IHP2.
    done.
  - destruct c as [c c'].
    specialize (IHP1 _ c).
    specialize (IHP2 _ c').
    destruct (decode P2 Q2 c').
    destruct (decode P1 Q1 c).
    simpl.
    rewrite <- IHP1.
    rewrite <- IHP2.
    done.
Defined.  

Lemma poly_plus_inv Q R Q' R' :
  poly_plus Q R = poly_plus Q' R' ->
  (Q = Q') * (R = R').
Proof.
  intros p.
  pose (c := encode _ _ p).
  simpl in c.
  destruct c as [c c'].
  pose (q := decode _ _ c).
  pose (q' := decode _ _ c').
  split; assumption.
Defined.