Proof: Difference between revisions
Added FreeBASIC
(Added FreeBASIC) |
|||
(7 intermediate revisions by 4 users not shown) | |||
Line 28:
3.1. using built-in natural numbers:
<
(evenp (+ x y))))</
=={{header|Agda}}==
<syntaxhighlight lang="agda">
module PeanoArithmetic where
-- 1.1. The natural numbers.
--
-- ℕ-formation: ℕ is set.
--
-- ℕ-introduction:
-- a ∈ ℕ | (
--
data ℕ : Set where
zero : ℕ
-- 1.2. The even natural numbers.
--
data 2×ℕ : ℕ → Set where
2+_ : {m : ℕ} → 2×ℕ m → 2×ℕ (
-- 1.3. The odd natural numbers.
--
data 2×ℕ+1 : ℕ → Set where
one : 2×ℕ+1
2+
-- 2.1. The rule of addition.
--
-- via ℕ-elimination.
--
infixl 6 _+_
_+_ : (k : ℕ) → (n : ℕ) → ℕ
zero + n = n
(suc m) + n = suc (m + n)
-- 3.1. Sum of any two even numbers is even.
--
-- This function takes any two even numbers and returns their sum as an even
-- number, this is the type, i.e. logical proposition, algorithm itself is a
Line 77 ⟶ 74:
-- typechecker performs that proof (by unification, so that this is a form of
-- compile-time verification).
--
even+even≡even : {m n : ℕ} → 2×ℕ m → 2×ℕ n → 2×ℕ (m + n)
even+even≡even
even+even≡even (2+ m) n = 2+ (even+even≡even m n)
-- The identity type
--
infix 4 _≡_
data _≡_ {A : Set} (m :
refl : m ≡ m
sym : {A : Set} → {m n :
sym refl = refl
trans : {A : Set} → {m n p :
trans refl n≡p = n≡p
-- refl, sym and trans forms an equivalence relation.
cong : {A B : Set} → (f : A → B) → {m n :
cong f refl = refl
-- 3.2.1. Direct proof of the associativity of addition using propositional
-- equality.
--
+-associative : (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-associative
+-associative (
-- Proof _of_ mathematical induction on the natural numbers.
--
-- P 0, ∀ x. P x → P (
--
ind : (P : ℕ → Set) → P
ind _ P₀ _
ind P P₀ next (
-- 3.2.2. The associativity of addition by induction (with propositional
-- equality, again).
--
+-associative′ : (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-associative′ m n p = ind P P₀ is m
Line 122 ⟶ 119:
P : ℕ → Set
P m = m + n + p ≡ m + (n + p)
P₀ : P
P₀ = refl
is : (m : ℕ) → P m → P (
is _ Pi = cong suc Pi
-- Syntactic sugar for equational reasoning (we don't use preorders here).
Line 131 ⟶ 128:
infix 4 _≋_
data _≋_ (m n : ℕ) : Set where
infix 1 begin_
begin_ : {m n : ℕ} → m ≋ n → m ≡ n
begin
infixr 2 _~⟨_⟩_
_~⟨_⟩_ : (m : ℕ){n p : ℕ} → m ≡ n → n ≋ p → m ≋ p
_ ~⟨ m≡n ⟩
infix
_∎ : (m : ℕ) → m ≋ m
_∎ _ =
-- Some helper proofs.
m+0≡m : (m : ℕ) → m +
m+0≡m
m+0≡m (
m+1+n≡1+m+n : (m n : ℕ) → m + (
m+1+n≡1+m+n
m+1+n≡1+m+n (
-- 3.3. The commutativity of addition using equational reasoning.
--
+-commutative : (m n : ℕ) → m + n ≡ n + m
+-commutative
+-commutative (
begin
suc (n + m)
~⟨ sym (m+1+n≡1+m+n n m) ⟩
n + suc m
∎
-- 3.4.
--
even+even≡odd : {m n : ℕ} → 2×ℕ m → 2×ℕ n → 2×ℕ+1 (m + n)
even+even≡odd
even+even≡odd _ _ = {!!}
-- ^
-- That gives
--
-- ?0 : 2×ℕ+1 (zero + zero)
-- ?1 : 2×ℕ+1 (
--
-- but 2×ℕ+1 (zero + zero) = 2×ℕ+1 0 which is uninhabited, so that this proof
-- can not be writen.
--
-- The absurd (obviously uninhabited) type.
--
-- ⊥-introduction is empty.
--
data ⊥ : Set where
-- The negation of a proposition.
--
infix 6 ¬_
¬_ : Set → Set
Line 195 ⟶ 196:
-- 4.1. Disproof or proof by contradiction.
--
-- To disprove even+even≡odd we assume that even+even≡odd and derive
-- absurdity, i.e. uninhabited type.
--
even+even≢odd : {m n : ℕ} → 2×ℕ m → 2×ℕ n → ¬ 2×ℕ+1 (m + n)
even+even≢odd
even+even≢odd
even+even≢odd (2+ m) n (2+₁ m+n) = even+even≢odd m n m+n
-- 4.2.
--
-- even+even≢even : {m n : ℕ} → 2×ℕ m → 2×ℕ n → ¬ 2×ℕ (m + n)
-- even+even≢even zero zero ()
-- ^
-- rejected with the following message:
--
-- 2×ℕ zero should be empty, but the following constructor patterns
-- are valid:
Line 216 ⟶ 217:
-- when checking that the clause even+even≢even zero zero () has type
-- {m n : ℕ} → 2×ℕ m → 2×ℕ n → ¬ 2×ℕ (m + n)
--
</syntaxhighlight>
=={{header|ATS}}==
Line 224 ⟶ 226:
The following seems similar, at least, to a completion of the task. The main problem I can see in it is it mostly consists of letting ATS do math it already knows on the ''recursion indices'' of the definition of addition. These happen to correspond to the natural numbers abstractly represented by the "prop" '''NATURAL'''.
Nevertheless, one can see that ATS is capable of some "abstract" reasoning. In fact, the prelude includes a recursive definition of multiplication, and in the [[Greatest_common_divisor#ATS|ATS entry for the greatest common divisor task]] I present ''practical'' (not "first principles") definitions of the gcd both by way of axioms and by recursive prop.
And the following does show, by total functions, how to construct a particular number (by counting up to it) and how to add (again by counting). That proofs of such things as "evens add up to evens" are then trivialized is perhaps a point ''in favor of'' ATS, ''as a systems programming language''.
<syntaxhighlight lang="ats">(* Let us do a little quasi-math in ATS, even though this is NOT an
intended use of the facilities. However, I DO consider the task a
good didactic exercise. *)
Line 376 ⟶ 380:
implement
main0 () =
println! ("Success!")</
{{out}}
Line 391 ⟶ 395:
<
contain enough to do a considerable amount of *informal* proof
about a program.
Line 493 ⟶ 497:
implement
main0 () =
println! ("Success!")</
{{out}}
Line 501 ⟶ 505:
=={{header|Coq}}==
<
Inductive nat : Set :=
| O : nat
Line 617 ⟶ 621:
intros. apply H1. apply (even_plus_even _ _ H H0).
Qed.
</syntaxhighlight>
=={{header|FreeBASIC}}==
{{trans|Phix}}
<syntaxhighlight lang="vbnet">Type Axioma
r As String
s As String
End Type
Dim Shared axiomas(1 To 6) As Axioma
axiomas(1).r = "even+1": axiomas(1).s = "odd"
axiomas(2).r = "even": axiomas(2).s = "2*int"
axiomas(3).r = "2*int+2*int": axiomas(3).s = "2*(int+int)"
axiomas(4).r = "(int+int)": axiomas(4).s = "int"
axiomas(5).r = "2*int": axiomas(5).s = "even"
axiomas(6).r = "odd": axiomas(6).s = "2*int+1"
Sub Proof(a As String, b As String)
'-- try to convert a into b using only the above axiomas
Dim As String w = a
Dim As String seen() ' -- (avoid infinite loops)
Dim As Integer i, k, hit
Do
Print Using """&"""; w
Redim Preserve seen(Lbound(seen) To Ubound(seen) + 1)
seen(Ubound(seen)) = w
If w = b Then Exit Do
hit = 0
For i = Lbound(axiomas) To Ubound(axiomas)
k = Instr(w, axiomas(i).r)
If k > 0 Then
w = Left(w, k - 1) & axiomas(i).s & Mid(w, k + Len(axiomas(i).r))
hit = i
Exit For
End If
Next i
Print " == ";
Loop Until hit = 0
Print Using "{""&"", ""&"", &}"; a; b; Iif(w = b, "true", "false")
End Sub
Proof("even+even", "even")
Proof("even+1", "odd")
'--bad proofs:
Proof("int", "even")
Sleep</syntaxhighlight>
{{out}}
<pre>"even+even"
== "2*int+even"
== "2*int+2*int"
== "2*(int+int)"
== "2*int"
== "even"
{"even+even", "even", true}
"even+1"
== "odd"
{"even+1", "odd", true}
"int"
{"int", "even", false}</pre>
=={{header|Go}}==
Line 629 ⟶ 693:
However, there is no obvious way to show that 3.2 and 3.3 must always be true (though you could argue that addition must be commutative because the 'addEven' function is symmetric in relation to its arguments). So all I've been able to do here is write functions to test these assertions for given even numbers whilst accepting that this doesn't constitute a proof for all such cases.
<
import "fmt"
Line 791 ⟶ 855:
testAssociative(genEven(numbers[7]), genEven(numbers[8]), genEven(numbers[9]))
}</
{{out}}
Line 819 ⟶ 883:
Using [http://www.haskell.org/haskellwiki/GADT GADTs] and [http://www.haskell.org/haskellwiki/GHC/Type_families type families] it is possible to write a partial adaptation of the Agda version:
<
module PeanoArithmetic where
Line 964 ⟶ 1,028:
--
-- since we have a "citizen" of an uninhabited type here (contradiction!).
-- </
See also [[Proof/Haskell]] for implementation of a small theorem prover.
Line 974 ⟶ 1,038:
These ways can be combined.
<syntaxhighlight lang="idris">
module Proof
Line 1,108 ⟶ 1,172:
exact evenNotOdd (EvSS ex) ossx
</syntaxhighlight>
=={{header|Isabelle}}==
<
imports Main
begin
Line 1,197 ⟶ 1,261:
by(auto intro: myeven.intros)
end</
=={{header|J}}==
Line 1,207 ⟶ 1,271:
So, these can be our definitions:
<
if. 0 = L. y do. context (,: ; ]) y return. end.
kernel=. > {: y
Line 1,239 ⟶ 1,303:
odd=: successor@even
defined=: '(zero not exists_in odd successor equals is_member_of addition even)'</
Here, '''even''' is a function which, given a natural number, produces a corresponding even natural number. '''odd''' is a similar function which gives us odd numbers.
Line 1,258 ⟶ 1,322:
# the sum of two even numbers can never be odd.
<
((even A) addition (even B)) is_member_of (even C)
((A addition B) addition C) equals (A addition (B addition C))
(A addition B) equals (B addition A)
not ((even A) addition (even B)) exists_in (odd C)
)</
Meanwhile, here is how the invalid proofs fail:
<
|assertion failure: assert</
and
<
|assertion failure: assert</
Line 1,282 ⟶ 1,346:
We use the Go method which means that this Nim version has the same limits. When translating, we did some adjustments: for instance, we use overloading of operators which allows a more natural way to express the operations.
<
type
Line 1,391 ⟶ 1,455:
testCommutative(newEvenNumber(numbers[8]), newEvenNumber(numbers[9]))
testAssociative(newEvenNumber(numbers[7]), newEvenNumber(numbers[8]), newEvenNumber(numbers[9]))</
{{out}}
Line 1,416 ⟶ 1,480:
Using GADT, we can port the Coq version to OCaml.
<syntaxhighlight lang="ocaml">
type zero = Zero
type 'a succ = Succ
Line 1,473 ⟶ 1,537:
plus_succ_left (plus_commutative a plus')
</syntaxhighlight>
=={{header|Omega}}==
<
EZ:: Even Z
ES:: Even n -> Even (S (S n))
Line 1,487 ⟶ 1,551:
even_plus EZ en = en
even_plus (ES em) en = ES (even_plus em en)
</syntaxhighlight>
=={{header|Phix}}==
Line 1,494 ⟶ 1,558:
Clearly 3.2 and 3.3 are not attempted, and I'm not sure which of 3.4/4.1/4.2 the last axiom is
closest to, or for that matter what the difference between them is supposed to be.
<!--<
<span style="color: #008080;">with</span> <span style="color: #008080;">javascript_semantics</span>
<span style="color: #008080;">constant</span> <span style="color: #000000;">axioms</span> <span style="color: #0000FF;">=</span> <span style="color: #0000FF;">{{</span><span style="color: #008000;">"even+1"</span><span style="color: #0000FF;">,</span><span style="color: #008000;">"odd"</span><span style="color: #0000FF;">},</span>
Line 1,532 ⟶ 1,596:
<span style="color: #000000;">proof</span><span style="color: #0000FF;">(</span><span style="color: #008000;">"int"</span><span style="color: #0000FF;">,</span><span style="color: #008000;">"even"</span><span style="color: #0000FF;">)</span>
<span style="color: #000000;">proof</span><span style="color: #0000FF;">(</span><span style="color: #008000;">"even+even"</span><span style="color: #0000FF;">,</span><span style="color: #008000;">"odd"</span><span style="color: #0000FF;">)</span>
<!--</
{{out}}
<pre>
Line 1,560 ⟶ 1,624:
Via <code>#lang cur</code>.
<
(require rackunit
Line 1,635 ⟶ 1,699:
(by-rewrite IHa)
display-focus ; show how the context and goal are after rewrite
reflexivity)</
{{out}}
Line 1,658 ⟶ 1,722:
=={{header|Raku}}==
Partial attempt only.
<syntaxhighlight lang="raku"
sub check ($type, @testee) {
Line 1,700 ⟶ 1,764:
# 4.1 Prove that the addition of any two even numbers cannot be odd
# 4.2 Try to prove that the addition of any two even numbers cannot be even (it should be rejected)
</syntaxhighlight>
{{out}}
<pre>Is 0 ∈ ℕ : True
Line 1,716 ⟶ 1,780:
Note that the only current implementation of Salmon is an interpreter that ignores proofs and doesn't try to check them, but in the future when there is an implementation that checks proofs, it should be able to check the proof in this Salmon code.
<
theorem(forall(x : even, y : even) ((x + y) in even))
proof
Line 1,744 ⟶ 1,808:
(x + y) in even because type_definition(even, L10);
};
};</
=={{header|Tcl}}==
Line 1,750 ⟶ 1,814:
{{works with|Tcl|8.5}}
<
datatype define Int = Zero | Succ val
datatype define EO = Even | Odd
Line 1,816 ⟶ 1,880:
} {
puts "\tevenOdd \[[list add $a $b]\] = [evenOdd [add $a $b]]"
}</
Output:
<pre>BASE CASE
Line 1,834 ⟶ 1,898:
=={{header|Twelf}}==
<
z : nat.
s : nat -> nat.
Line 1,878 ⟶ 1,942:
%worlds () (sum-evens _ _ _ _).
%total D (sum-evens D _ _ _).
</syntaxhighlight>
=={{header|Wren}}==
Line 1,884 ⟶ 1,948:
{{libheader|Wren-fmt}}
Most of what was said in the preamble to the Go entry applies equally to Wren though, as Wren is dynamically typed, we have to rely on runtime type checks.
<
// Represents a natural number.
Line 2,054 ⟶ 2,118:
testCommutative.call(EvenNumber.new(numbers[8]), EvenNumber.new(numbers[9]))
testAssociative.call(EvenNumber.new(numbers[7]), EvenNumber.new(numbers[8]), EvenNumber.new(numbers[9]))</
{{out}}
|