Matita
1 program
Added 2026-02-10T13:36:50Z
Agent: claude-codeModel: claude-opus-4-6WebSearch: disabled
Evidence
Report issue
View issues
Aliases: —
Provenance: commit 59df8a0739 · authored 2026-02-10T14:41:19+01:00 · agent claude-code · model claude-opus-4-6
Sources mentioning this language
2 sources · pl_id:
pl/matitaRelated languages
LLM-contributed programs
Natural Numbers and Commutativity of Addition
Provenance: commit 59df8a0739 · authored 2026-02-10T14:41:19+01:00 · agent claude-code · model claude-opus-4-6 · WebSearch disabled
include "basics/pts.ma".
inductive nat : Type[0] ≝
| O : nat
| S : nat → nat.
let rec plus n m on n ≝
match n with
[ O ⇒ m
| S p ⇒ S (plus p m)
].
let rec times n m on n ≝
match n with
[ O ⇒ O
| S p ⇒ plus m (times p m)
].
theorem plus_O_n : ∀n:nat. plus O n = n.
#n normalize //
qed.
theorem plus_n_O : ∀n:nat. plus n O = n.
#n elim n
[ normalize //
| #p #IH normalize >IH //
]
qed.
theorem plus_n_Sm : ∀n,m:nat. S (plus n m) = plus n (S m).
#n #m elim n
[ normalize //
| #p #IH normalize >IH //
]
qed.
theorem plus_comm : ∀n,m:nat. plus n m = plus m n.
#n #m elim n
[ normalize >(plus_n_O m) //
| #p #IH normalize >IH >(plus_n_Sm m p) //
]
qed.
Real programs from Software Heritage
No SWH evidence indexed yet for this language. (Either the SWH mining hasn't reached this language's extensions, or no matching files exist in the archive.)