Skip to content

Instantly share code, notes, and snippets.

@co-dan co-dan/poly.v
Created Sep 9, 2017

Embed
What would you like to do?
Encode-decode for the polynomials
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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.