Proof: Difference between revisions
OCaml version (now possible with GADT's)
(→{{header|Mathematica}}: Delete the wrong answer) |
(OCaml version (now possible with GADT's)) |
||
Line 8:
{{omit from|Java}}
{{omit from|MUMPS|Not a typed language}}
{{omit from|OCaml}}▼
{{omit from|Python}}
{{omit from|M4}}
Line 650 ⟶ 649:
As an aside, note that peano numbers show us that numbers can represent recursive processes.
Using GADT, we can port the Coq version to OCaml.
<lang OCaml>
type zero = Zero
type 'a succ = Succ
(* 1.1 *)
type _ nat =
| Zero : zero nat
| Succ : 'a nat -> 'a succ nat
(* 1.2 *)
type _ even =
| Even_zero : zero even
| Even_ss : 'a even -> 'a succ succ even
(* 2.1: define the addition relation *)
type (_, _, _) plus =
| Plus_zero : ('a, zero, 'a) plus
| Plus_succ : ('a, 'b, 'c) plus -> ('a, 'b succ, 'c succ) plus
(* 3.1 *)
(* Define the property: there exists a number 'sum that is the sum of 'a and 'b and is even. *)
type ('a, 'b) exists_plus_even = Exists_plus_even : ('a, 'b, 'sum) plus * 'sum even -> ('a, 'b) exists_plus_even
(* The proof that if a and b are even, there exists sum that is the sum of a and b that is even.
This is a valid proof since it terminated, and it is total (no assert false, and the exhaustiveness
test of pattern matching doesn't generate a warning) *)
let rec even_plus_even : type a b. a even -> b even -> (a, b) exists_plus_even =
fun a_even b_even ->
match b_even with
| Even_zero ->
Exists_plus_even (Plus_zero, a_even)
| Even_ss b_even' ->
let Exists_plus_even (plus, even) = even_plus_even a_even b_even' in
Exists_plus_even (Plus_succ (Plus_succ plus), Even_ss even)
</lang>
=={{header|Omega}}==
| |||