congruence_fail.v

Goal forall (f g : nat -> nat),
  (forall x, f x = f (g x)) ->
  (forall x, f (g x) = f (S x)) ->
  f 0 = f 100.
Proof.
  intros f g H H0.
  Fail congruence.
  repeat rewrite <- H0, <- H.
  reflexivity.
Qed.

gistfile1.txt

Lemma add0n n : 0 + n = n. Proof. reflexivity. Qed.
 
Lemma addSn n m : S n + m = S (n + m). Proof. reflexivity. Qed.

Lemma addn0 n : n + 0 = n.
Proof.
  set (add0n := add0n). set (addSn := addSn).
  induction n; congruence.
Qed.
 
Lemma addnS n m : n + S m = S (n + m).
Proof.
  set (add0n := add0n). set (addSn := addSn).
  induction n; congruence.
Qed.
 
Lemma addnC n m : n + m = m + n.
Proof.
  set (add0n := add0n). set (addSn := addSn).
  set (addn0 := addn0). set (addnS := addnS).
  induction n; congruence.
Qed.

Lemma addnA a b c : a + b + c = a + (b + c).
  set (add0n := add0n). set (addSn := addSn).
  set (addn0 := addn0). set (addnS := addnS).
  induction a; congruence.
Qed.

Lemma mul0n n : 0 * n = 0.
Proof. reflexivity. Qed.

Lemma mulSn n m : S n * m = m + n * m.
Proof. reflexivity. Qed.

Lemma muln0 n : n * 0 = 0.
Proof.
  set (add0n := add0n).
  set (mul0n := mul0n). set (mulSn := mulSn).
  induction n; congruence.
Qed.

Lemma mulnS n m : n * S m = n + n * m.
Proof.
  set (add0n := add0n). set (addSn := addSn).
  set (addn0 := addn0). set (addnS := addnS).
  set (addnC := addnC). set (addnA := addnA).
  set (mul0n := mul0n). set (mulSn := mulSn).
  set (muln0 := muln0).
  induction n; congruence.
Qed.

Lemma mulnC n m : n * m = m * n.
Proof.
  set (add0n := add0n). set (addSn := addSn).
  set (addn0 := addn0). set (addnS := addnS).
  set (addnC := addnC). set (addnA := addnA).
  set (mul0n := mul0n). set (mulSn := mulSn).
  set (muln0 := muln0). set (mulnS := mulnS).
  induction n; congruence.
Qed.

Lemma mulnDl a b c : (a + b) * c = a * c + b * c.
Proof.
  set (add0n := add0n). set (addSn := addSn).
  set (addn0 := addn0). set (addnS := addnS).
  set (addnC := addnC). set (addnA := addnA).
  set (mul0n := mul0n). set (mulSn := mulSn).
  set (muln0 := muln0). set (mulnS := mulnS).
  set (mulnC := mulnC).
  induction a; congruence.
Qed.

Lemma mulnA a b c : a * b * c = a * (b * c).
Proof.
  set (add0n := add0n). set (addSn := addSn).
  set (addn0 := addn0). set (addnS := addnS).
  set (addnC := addnC). set (addnA := addnA).
  set (mul0n := mul0n). set (mulSn := mulSn).
  set (muln0 := muln0). set (mulnS := mulnS).
  set (mulnC := mulnC). set (mulnDl := mulnDl).
  induction a; congruence.
Qed.