coq_practice_37.v

Require Import SetoidClass.
Require Import Arith.

Record int := {
  Ifst : nat;
  Isnd : nat
}.

Program Instance ISetoid : Setoid int := {|
  equiv x y := Ifst x + Isnd y = Ifst y + Isnd x
|}.
Next Obligation.
Proof.
  intuition.
  unfold Transitive.
  intros.
  assert (Ifst x + Isnd z + (Isnd y + Ifst y) = Ifst z + Isnd x + Isnd y + Ifst y).
    rewrite Plus.plus_permute_2_in_4.
    rewrite H.
    replace (Isnd z + Ifst y) with (Ifst y + Isnd z) by ring.
    rewrite H0.
    ring.
  apply (plus_reg_l (Ifst x + Isnd z ) (Ifst z + Isnd x) (Isnd y + Ifst y)).
  rewrite plus_comm.
  rewrite H1.
  ring.
  (* ここを埋める *)
Qed.

Definition zero : int := {|
  Ifst := 0;
  Isnd := 0
|}.

Definition int_minus(x y : int) : int := {|
  Ifst := Ifst x + Isnd y;
  Isnd := Isnd x + Ifst y
|}.

Lemma int_sub_diag : forall x, int_minus x x == zero.
Proof.
  (* ここを埋める *)
   intros.
   unfold int_minus.
   simpl.
   ring.
Qed.

(* まず、int_minus_compatを証明せずに、下の2つの証明を実行して、どちらも失敗することを確認せよ。*)
(* 次に、int_minus_compatを証明し、下の2つの証明を実行せよ。 *)

Instance int_minus_compat : Proper (equiv ==> equiv ==> equiv) int_minus.
Proof.
  unfold Proper.
  simpl.
  unfold int_minus.
  intro.
  intros.
  intro.
  intros.
  simpl.
  assert ((Ifst x + Isnd x0 + (Isnd y + Ifst y0)) = ((Ifst x + Isnd y) + ( Ifst y0 + Isnd x0))).
  ring.
  rewrite H1.
  rewrite H.
  rewrite <-  H0.
  ring.
(* ここを埋める *)
Qed.



Goal forall x y, int_minus x (int_minus y y) == int_minus x zero.
Proof.
  intros x y.
  rewrite int_sub_diag.
  reflexivity.
Qed.

Goal forall x y, int_minus x (int_minus y y) == int_minus x zero.
Proof.
  intros x y.
  setoid_rewrite int_sub_diag.
  reflexivity.
Qed.