Skip to content

Instantly share code, notes, and snippets.

@satos---jp
Created June 1, 2014 08:16
Show Gist options
  • Save satos---jp/89c84c2c79d14ec6a589 to your computer and use it in GitHub Desktop.
Save satos---jp/89c84c2c79d14ec6a589 to your computer and use it in GitHub Desktop.
Require Import ZArith.
Section Principal_Ideal.
Variable a : Z.
Definition pi : Set := { x : Z | ( a | x )%Z }.
Program Definition plus(a b : pi) : pi := (a + b)%Z.
Next Obligation.
unfold proj1_sig.
unfold Z.divide.
destruct a0.
destruct b.
destruct d.
destruct d0.
exists (x1+x2)%Z.
rewrite H.
rewrite H0.
ring.
Qed.
Program Definition mult(a : Z) (b : pi) : pi := (a * b)%Z.
Next Obligation.
unfold proj1_sig.
unfold Z.divide.
destruct b.
destruct d.
rewrite H.
exists (a0 * x0)%Z.
ring.
Qed.
End Principal_Ideal.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment