Proof: Difference between revisions
Added FreeBASIC
(→{{header|Agda}}: Fixed Agda example) |
(Added FreeBASIC) |
||
| (3 intermediate revisions by 2 users not shown) | |||
Line 36:
-- 1.1. The natural numbers.
--
-- ℕ-formation: ℕ is set.
--
-- ℕ-introduction:
--
--
data ℕ : Set where
zero : ℕ
suc : (n : ℕ) → ℕ
-- 2.1. The rule of addition.▼
-- ▼
-- via ℕ-elimination.▼
-- ▼
infixl 6 _+_▼
_+_ : ℕ → ℕ → ℕ▼
0 + n = n▼
suc m + n = suc (m + n)▼
-- 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 : ℕ) → ℕ
▲(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 (for propositional equality).
--
infix 4 _≡_
data _≡_ {A : Set} (m : A) : A → Set where
Line 101 ⟶ 98:
-- 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 (suc m) n p = cong suc (+-associative m n p)
-- Proof _of_ mathematical induction on the natural numbers.
--
-- P 0, ∀ x. P x → P (suc x) | ∀ x. P x.
--
ind : (P : ℕ → Set) → P
ind _ P₀ _
ind P P₀ next (suc n) = next n (ind P P₀ next n)
-- 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
Line 148 ⟶ 145:
-- Some helper proofs.
m+0≡m : (m : ℕ) → m +
m+0≡m
m+0≡m (suc m) = cong suc (m+0≡m m)
m+1+n≡1+m+n : (m n : ℕ) → m + (
m+1+n≡1+m+n
m+1+n≡1+m+n (suc m) n = cong suc (m+1+n≡1+m+n m n)
-- 3.3. The commutativity of addition using equational reasoning.
--
+-commutative : (m n : ℕ) → m + n ≡ n + m
+-commutative
+-commutative (suc m) n =
begin
~⟨ refl ⟩
~⟨ cong suc (+-commutative m n) ⟩
~⟨ sym (m+1+n≡1+m+n n 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 200 ⟶ 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 626 ⟶ 622:
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 1,892 ⟶ 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.
<syntaxhighlight lang="
// Represents a natural number.
| |||