読者です 読者をやめる 読者になる 読者になる

にわとり小屋でのプログラミング ブログ

名古屋のCoqエンジニアです。日記は勘で書いてるところがあるので細かいとこが違うことがあります。

PeanoPositive.v

まずこの前のコードに引き算のレンマを加えて、PeanoPositive.vとしてまとめた。

Inductive mypositive : Set :=
 | I : mypositive
 | myS : mypositive -> mypositive.

Fixpoint myPplus mp1 mp2 {struct mp1} := match mp1 with
  | I => myS mp2
  | myS mp1' => myS (myPplus mp1' mp2)
  end.
Fixpoint myPmult mp1 mp2 {struct mp1} := match mp1 with
  | I => mp2
  | myS mp1' => myPplus mp2 (myPmult mp1' mp2)
  end.

Require Import ZArith.
Require Import BinPos.
Definition two := myS I.
Definition ten := myS (myS (myS (myS (myS (myS (myS (myS (myS I)))))))).
Fixpoint mypositive_of_positive p := match p with
  | xH => I
  | xO p' => myPmult two (mypositive_of_positive p')
  | xI p' => myS (myPmult two (mypositive_of_positive p'))
  end.
Fixpoint positive_of_mypositive mp := match mp with
  | I => xH
  | myS mp' => Psucc (positive_of_mypositive mp')
  end.


(** (Mypplus,Pplus) and (mypmult,Pmult) are Homomorphisms *)
Theorem hom_myPplus_Pplus : forall mp1 mp2:mypositive,
  positive_of_mypositive (myPplus mp1 mp2)
  = Pplus (positive_of_mypositive mp1) (positive_of_mypositive mp2).
Proof.
intros mp1 mp2; induction mp1.
 unfold myPplus in |- *.
   unfold positive_of_mypositive in |- *; fold positive_of_mypositive in |- *.
   apply Pplus_one_succ_l.
simpl in |- *.
  rewrite IHmp1 in |- *.
  rewrite Pplus_succ_permute_l in |- *.
  reflexivity.
Qed.



Lemma Pmult_succ_l : forall p q:positive,
 Pmult (Psucc p) q = Pplus q (Pmult p q).
Proof.
intros p q; rewrite Pplus_one_succ_l in |- *.
rewrite Pmult_plus_distr_r in |- *.
simpl in |- *; reflexivity.
Qed.



Theorem hom_myPmult_Pmult : forall mp1 mp2:mypositive,
  positive_of_mypositive (myPmult mp1 mp2)
  = Pmult (positive_of_mypositive mp1) (positive_of_mypositive mp2).
Proof.
intros mp1 mp2; induction mp1.
 simpl in |- *; reflexivity.
simpl in |- *.
  rewrite hom_myPplus_Pplus in |- *.
  rewrite IHmp1 in |- *.
  rewrite Pmult_succ_l in |- *.
  reflexivity.
Qed.


(** Mypositive_of_positive and inversion are INJECTIVE and SURJECTIVE *)


Lemma myPplus_succ_permute_r : forall myp myq:mypositive,
  myPplus myp (myS myq) = myS (myPplus myp myq).
Proof.
intro myp; induction myp.
 intro; simpl in |- *.
   reflexivity.
intro myq; simpl in |- *.
  rewrite IHmyp in |- *; reflexivity.
Qed.


Lemma succ_hom : forall p:positive, 
 mypositive_of_positive (Psucc p) = myS (mypositive_of_positive p).
Proof.
intro p; induction p.
 simpl in |- *.
   rewrite IHp in |- *.
   simpl in |- *.
   rewrite myPplus_succ_permute_r in |- *.
   reflexivity.
simpl in |- *.
  reflexivity.
simpl in |- *.
  reflexivity.
Qed.

Theorem myP_P_injective : forall mp:mypositive,
 mypositive_of_positive (positive_of_mypositive mp) = mp.
Proof.
intro mp; induction mp.
 simpl in |- *; reflexivity.
simpl in |- *.
  rewrite succ_hom in |- *.
  rewrite IHmp in |- *; reflexivity.
Qed.

Theorem myP_P_surjective : forall p:positive,
 positive_of_mypositive (mypositive_of_positive p) = p.
Proof.
intro p; induction p.
 simpl in |- *.
   rewrite hom_myPplus_Pplus in |- *.
   rewrite IHp in |- *.
   rewrite xI_succ_xO in |- *; rewrite <- Pplus_diag in |- *.
   reflexivity.
simpl in |- *.
  rewrite hom_myPplus_Pplus in |- *.
  rewrite IHp in |- *.
  rewrite Pplus_diag in |- *; reflexivity.
simpl in |- *; reflexivity.
Qed.

(** Lemmas *)
Lemma myPplus_comm : forall mp mq:mypositive,
  myPplus mp mq = myPplus mq mp.
Proof.
intros mp mq.
rewrite <- myP_P_injective in |- *.
rewrite hom_myPplus_Pplus in |- *.
rewrite Pplus_comm in |- *.
rewrite <- hom_myPplus_Pplus in |- *.
rewrite myP_P_injective in |- *; reflexivity.
Qed.

Lemma myPplus_assoc: forall mp mq mr : mypositive,
 myPplus mp (myPplus mq mr) = myPplus (myPplus mp mq) mr.
Proof.
intros mp mq mr.
rewrite <- myP_P_injective in |- *.
rewrite hom_myPplus_Pplus in |- *.
rewrite hom_myPplus_Pplus in |- *.
rewrite <- Pplus_assoc in |- *.
rewrite <- hom_myPplus_Pplus in |- *.
rewrite <- hom_myPplus_Pplus in |- *.
rewrite myP_P_injective in |- *; reflexivity.
Qed.


Lemma myPmult_plus_distr_l: forall mp mq mr : mypositive,
 myPmult mp (myPplus mq mr) = myPplus (myPmult mp mq) (myPmult mp mr).
Proof.
intros mp mq mr; rewrite <- myP_P_injective in |- *.
rewrite hom_myPplus_Pplus in |- *; rewrite hom_myPmult_Pmult in |- *;
 rewrite hom_myPmult_Pmult in |- *.
rewrite <- Pmult_plus_distr_l in |- *.
rewrite <- hom_myPplus_Pplus in |- *; rewrite <- hom_myPmult_Pmult in |- *.
rewrite myP_P_injective in |- *; reflexivity.
Qed.

Lemma myPmult_plus_distr_r: forall mp mq mr : mypositive, 
 myPmult (myPplus mp mq) mr = myPplus (myPmult mp mr) (myPmult mq mr).
Proof.
intros mp mq mr; rewrite <- myP_P_injective in |- *.
rewrite hom_myPplus_Pplus in |- *; rewrite hom_myPmult_Pmult in |- *;
 rewrite hom_myPmult_Pmult in |- *.
rewrite <- Pmult_plus_distr_r in |- *.
rewrite <- hom_myPplus_Pplus in |- *; rewrite <- hom_myPmult_Pmult in |- *.
rewrite myP_P_injective in |- *; reflexivity.
Qed.

Lemma myPmult_1_r: forall mp : mypositive, myPmult mp I = mp.
Proof.
intro mp; induction mp.
 simpl in |- *; reflexivity.
 simpl in |- *; rewrite IHmp in |- *; reflexivity.
Qed.


Lemma myPmult_comm: forall mp mq : mypositive,
 myPmult mp mq = myPmult mq mp.
Proof.
intros mp mq.
rewrite <- myP_P_injective in |- *.
rewrite hom_myPmult_Pmult in |- *.
rewrite Pmult_comm in |- *.
rewrite <- hom_myPmult_Pmult in |- *.
rewrite myP_P_injective in |- *; reflexivity.
Qed.

Lemma myPmult_assoc: forall mp mq mr : mypositive, 
 myPmult mp (myPmult mq mr) = myPmult (myPmult mp mq) mr.
Proof.
intros mp mq mr.
rewrite <- myP_P_injective in |- *.
rewrite hom_myPmult_Pmult in |- *.
rewrite hom_myPmult_Pmult in |- *.
rewrite <- Pmult_assoc in |- *.
rewrite <- hom_myPmult_Pmult in |- *.
rewrite <- hom_myPmult_Pmult in |- *.
rewrite myP_P_injective in |- *; reflexivity.
Qed.



(** Ordering *)
Fixpoint myPcompare x y {struct y} : comparison :=
 match x,y with
 | I,I => Eq
 | myS _, I => Gt
 | I, myS _ => Lt
 | myS x', myS y' => myPcompare x' y'
 end.

Definition Myp_lt x y := myPcompare x y = Lt.
Definition Myp_le x y := x=y \/ Myp_lt x y.


Theorem MypEq_eq : forall x y:mypositive,
  myPcompare x y = Eq -> x = y.
Proof.
intro x; induction x; intro y; induction y.
 intro; reflexivity.
unfold myPcompare in |- *; intro eq;  discriminate eq.
unfold myPcompare in |- *; intro eq;  discriminate eq.
simpl in |- *; intro H; rewrite (IHx y H) in |- *; reflexivity.
Qed.

Lemma ord4 : forall x y:mypositive,
 Myp_lt x y -> not (Myp_lt y x).
Proof.
intro x; induction x; intro y; induction y.
 intro lt; unfold Myp_lt in lt.
   unfold myPcompare in lt.
    discriminate lt.
intro; intro lt.
  unfold Myp_lt in lt.
  unfold myPcompare in lt.
   discriminate lt.
intro lt; unfold Myp_lt in lt; unfold myPcompare in lt;  discriminate lt.
unfold Myp_lt in |- *; simpl in |- *.
  unfold Myp_lt in IHx.
  apply IHx.
Qed.

Lemma ord5 : forall x y z:mypositive,
 Myp_lt x y /\ Myp_lt y z -> Myp_lt x z.
Proof.
intro x; induction x; intro y; induction y; intro z; induction z.
 intro H; elim H; intros H1 H2.
   unfold Myp_lt in H1; unfold myPcompare in H1;  discriminate H1.
intro H; elim H; intro H1; unfold Myp_lt in H1; unfold myPcompare in H1;
  discriminate H1.
intro H; elim H; intros H1 H2.
  elim (ord4 I (myS y) H1).
  apply H2.
intro; unfold Myp_lt in |- *; unfold myPcompare in |- *; reflexivity.
intro H; elim H; intros H1 H2; unfold Myp_lt in H2; unfold myPcompare in H2;
  discriminate H2.
intro H; elim H; intro H1; unfold Myp_lt in H1; unfold myPcompare in H1;
  discriminate H1.
intro H; elim H; intros H1 H2; unfold Myp_lt in H2; unfold myPcompare in H2;
  discriminate H2.
unfold Myp_lt in |- *; simpl in |- *.
  unfold Myp_lt in IHx; apply IHx.
Qed.

Require Import orderedset.


Lemma ord1 : forall x:mypositive, Myp_le x x.
Proof.
apply (t1 mypositive Myp_lt).
 split; unfold Myp_le in |- *; intro; assumption.
unfold orderedset.o4 in |- *; apply ord4.
unfold orderedset.o5 in |- *; apply ord5.
Qed.

Lemma ord2 : forall x y:mypositive,
 Myp_le x y /\ Myp_le y x -> x = y.
Proof.
apply (t2 mypositive Myp_lt).
 split; unfold Myp_le in |- *; intro; assumption.
unfold orderedset.o4 in |- *; apply ord4.
unfold orderedset.o5 in |- *; apply ord5.
Qed.

Lemma ord3 : forall x y z:mypositive,
 Myp_le x y /\ Myp_le y z -> Myp_le x z.
Proof.
 apply (t3 mypositive Myp_lt).
 split; unfold Myp_le in |- *; intro; assumption.
unfold orderedset.o4 in |- *; apply ord4.
unfold orderedset.o5 in |- *; apply ord5.
Qed.


(** Pcompare lemmas *)
Lemma Pcompare_lt_xH_lt : forall p:positive,
 Pcompare xH p Lt = Lt.
Proof.
intro p; case p; simpl in |- *; trivial.
Qed.

Lemma Pcompare_gt_lt_succ : forall p q:positive,
 Pcompare p q Gt = Pcompare (Psucc p) q Lt.
Proof.
intro p; induction p; intro q; case q; simpl in |- *.
 apply IHp.
apply IHp.
reflexivity.
intro mm; reflexivity.
intro mm; reflexivity.
reflexivity.
intro p; rewrite Pcompare_lt_xH_lt in |- *; reflexivity.
intro p; rewrite Pcompare_lt_xH_lt in |- *; reflexivity.
reflexivity.
Qed.

Lemma Pcompare_lt_gt_succ : forall p q:positive,
 Pcompare p q Lt = Pcompare p (Psucc q) Gt.
Proof.
intro p; induction p; intro q; case q; simpl in |- *.
 apply IHp.
intro mm; reflexivity.
case p; simpl in |- *; trivial.
apply IHp.
intro mm; reflexivity.
case p; trivial.
intro mm; reflexivity.
intro mm; reflexivity.
reflexivity.
Qed.

Theorem Pcompare_succ : forall (p q:positive) (C:comparison),
  Pcompare (Psucc p)(Psucc q) C = Pcompare p q C.
Proof.
intro p; induction p; intros q C; case q; simpl in |- *.
 intro q'; apply IHp.
intro q'; rewrite Pcompare_gt_lt_succ in |- *; reflexivity.
case p; simpl in |- *; trivial.
intro q'; rewrite Pcompare_lt_gt_succ in |- *; reflexivity.
intro mm; reflexivity.
case p; trivial.
intro p; case p; trivial.
intro p; case p; trivial.
reflexivity.
Qed.

(** 順序同型 *)
Theorem hom_ord_mypcompare_pcompare : forall x y:mypositive,
  myPcompare x y
   = Pcompare (positive_of_mypositive x) (positive_of_mypositive y) Eq.
Proof.
intro x; induction x; intro y; case y; simpl in |- *.
 reflexivity.
intro m; case (positive_of_mypositive m); simpl in |- *; trivial.
case (positive_of_mypositive x); trivial.
intro y'; rewrite Pcompare_succ in |- *.
  apply IHx.
Qed.


(**Pminus*)
Theorem Pminus_succ_one_l : forall p:positive,
  Pminus (Psucc p) xH = p.
Proof.
intro p; induction p.
 simpl in |- *.
   unfold Pminus in |- *.
   unfold Pminus_mask in |- *.
   generalize IHp.
   case p.
  intro; simpl in |- *.
    unfold Pminus in |- *.
    unfold Pminus_mask in |- *.
    intro eq; rewrite eq in |- *; reflexivity.
 intro p'; unfold Psucc in |- *; unfold Pminus in |- *.
   unfold Pminus_mask in |- *.
   unfold Pdouble_minus_one in |- *.
   intro; reflexivity.
 intro; simpl in |- *; reflexivity.
simpl in |- *.
  unfold Pminus in |- *.
  unfold Pminus_mask in |- *.
  reflexivity.
  unfold Psucc in |- *; unfold Pminus in |- *.
  unfold Pminus_mask in |- *.
  unfold Pdouble_minus_one in |- *.
  reflexivity.
Qed.


    
Theorem Pminus_mask_carry_succ_l : forall p q : positive,
  Pminus_mask p q = Pminus_mask_carry (Psucc p) q.
Proof.
intro p; induction p; intro q; case q; simpl in |- *; try reflexivity.
 intro; rewrite IHp in |- *; reflexivity.
intro; rewrite IHp in |- *; reflexivity.
case p; simpl in |- *; try reflexivity.
  intro p'; induction p'; simpl in |- *; try reflexivity.
   injection IHp'.
  intro eq; rewrite eq in |- *; reflexivity.
intro p; case p; simpl in |- *; reflexivity.
intro p; case p; simpl in |- *; reflexivity.
Qed.


Theorem Pminus_mask_carry_succ_r : forall p q : positive,
  Pminus_mask_carry p q = Pminus_mask p (Psucc q).
Proof.
intro p; induction p; intro q; case q; try simpl in |- *; try reflexivity.
 intro; rewrite IHp in |- *; reflexivity.
case p; try simpl in |- *; try reflexivity.
intro; rewrite IHp in |- *; reflexivity.
case p; try simpl in |- *; try reflexivity.
Qed.

Theorem Pminus_mask_succ_succ : forall p q:positive,
  Pminus_mask (Psucc p)(Psucc q) = Pminus_mask p q.
Proof.
intro p; induction p; intro q; case q; simpl in |- *.
 intro; rewrite IHp in |- *; reflexivity.
intro; rewrite Pminus_mask_carry_succ_l in |- *; reflexivity.
case p; simpl in |- *; try reflexivity.
  intro p'; induction p'; simpl in |- *; try reflexivity.
   injection IHp'; intro eq; rewrite eq in |- *; reflexivity.
intro; rewrite Pminus_mask_carry_succ_r in |- *; reflexivity.
intro; reflexivity.
case p; simpl in |- *; try reflexivity.
intro p; case p; simpl in |- *; reflexivity.
intro p; case p; simpl in |- *; reflexivity.
reflexivity.
Qed.

Theorem Pminus_succ_succ : forall p q:positive,
  Pminus (Psucc p)(Psucc q) = Pminus p q.
Proof.
intros p q; unfold Pminus in |- *; rewrite Pminus_mask_succ_succ in |- *;
 reflexivity.
Qed.


(** myPminus *)
Fixpoint myPminus x y {struct y} := match x,y with
 | I,_ => I
 | myS x',I => x'
 | myS x',myS y' => myPminus x' y'
 end.

Theorem hom_myPminus_Pminus : forall x y:mypositive,
 positive_of_mypositive (myPminus x y)
  = Pminus (positive_of_mypositive x)(positive_of_mypositive y).
Proof.
intro x; induction x.
 intro y; case y; simpl in |- *.
  unfold Pminus in |- *.
    unfold Pminus_mask in |- *.
    reflexivity.
 intro m; case (Psucc (positive_of_mypositive m)); unfold Pminus in |- *;
  unfold Pminus_mask in |- *; reflexivity.
intro y; case y.
 simpl in |- *.
   rewrite Pminus_succ_one_l in |- *; reflexivity.
intro; simpl in |- *.
  rewrite IHx in |- *.
  rewrite Pminus_succ_succ in |- *; reflexivity.
Qed.