35 lines
845 B
Coq
35 lines
845 B
Coq
Inductive nat : Set :=
|
|
| O : nat
|
|
| S : nat -> nat.
|
|
|
|
Require Import Coq.Arith.Plus.
|
|
|
|
Definition mult_comm : forall n m, n * m = m * n.
|
|
Proof.
|
|
intros. elim n.
|
|
auto with arith.
|
|
intros. simpl in |- *. elim mult_n_Sm. elim H. apply plus_comm.
|
|
Qed.
|
|
|
|
Definition mult_comm := fun n:nat
|
|
=> fix rec (m : nat)
|
|
: n * m = m * n
|
|
:= match m as m return n * m = m * n with
|
|
| O => sym_eq (mult_n_O _)
|
|
| S pm => match rec pm in _ = dep return _ = n + dep
|
|
with refl_equal =>
|
|
match mult_n_Sm _ _ in _ = dep return dep = _
|
|
with refl_equal => plus_comm _ _ end
|
|
end
|
|
end.
|
|
|
|
Definition mult_comm := fun n:nat
|
|
=> nat_ind (fun m => n * m = m * n)
|
|
(sym_eq (mult_n_O _))
|
|
(fun _ rec =>
|
|
eq_ind _ (fun dep => _ = n + dep)
|
|
(eq_ind _ (fun dep => dep = _)
|
|
(plus_comm _ _) _ (mult_n_Sm _ _))
|
|
_ rec).
|
|
|