Anonymous user
Proof: Difference between revisions
Added Idris
(Mathematica) |
(Added Idris) |
||
Line 428:
See also [[Proof/Haskell]] for implementation of a small theorem prover.
=={{header|Idris}}==
Idris supports two types of proofs: using tactics, like Coq, or just write functions like Agda.
These ways can be combined.
<lang Idris>
module Proof
-- Enable terminator chercker by default
%default total
-- 1.1 Natural numbers
%elim
data MyNat
= Z
| S MyNat
-- 1.2 Even naturals
%elim
data EvNat : MyNat -> Type where
EvO : EvNat Z
EvSS : EvNat x -> EvNat (S (S x))
-- 1.3 Odd naturals
%elim
data OddNat : MyNat -> Type where
Odd1 : OddNat (S Z)
OddSS : OddNat x -> OddNat (S (S x))
-- 2.1 addition
infixl 4 :+
(:+) : MyNat -> MyNat -> MyNat
(:+) Z b = b
(:+) (S a) b = S (a :+ b)
-- 3.1, Prove that the addition of any two even numbers is even.
evensPlus1 : {a : MyNat} -> {b : MyNat} -> (EvNat a) -> (EvNat b) -> (EvNat (a :+ b))
evensPlus1 ea eb = ?proof31
congS : {a : MyNat} -> {b : MyNat} -> (a = b) -> (S a = S b)
congS refl = refl
evensPlus2 : {a : MyNat} -> {b : MyNat} -> (EvNat a) ->(EvNat b) -> (EvNat (a :+ b))
evensPlus2 EvO eb = eb
evensPlus2 {a=(S (S a))} (EvSS ea) eb = EvSS (evensPlus2 ea eb)
-- 3.2 Prove that the addition is always associative.
plusAssoc : (a : MyNat) -> (b : MyNat) -> (c : MyNat) -> (a :+ b) :+ c = a :+ (b :+ c)
plusAssoc Z b c = refl
plusAssoc (S a) b c = congS (plusAssoc a b c)
-- 3.3 Prove that the addition is always commutative.
plus0_r : (a : MyNat) -> a :+ Z = a
plus0_r Z = refl
plus0_r (S a) = congS (plus0_r a)
plusS_r : (a : MyNat) -> (b : MyNat) -> a :+ S b = S (a :+ b)
plusS_r Z b = refl
plusS_r (S a) b = congS (plusS_r a b)
plusComm : (a : MyNat) -> (b : MyNat) -> a :+ b = b :+ a
plusComm a b = ?proof33
-- 4.1 Prove that the addition of any two even numbers cannot be odd.
evenNotOdd : (ea : EvNat a) -> (oa : OddNat a) -> _|_
evenNotOdd (EvSS e) (OddSS o) = evenNotOdd e o
evensPlusNotOdd : (ea : EvNat a) -> (eb : EvNat b) -> (OddNat (a :+ b)) -> _|_
evensPlusNotOdd EvO (EvSS eb) (OddSS ob) = evenNotOdd eb ob
evensPlusNotOdd (EvSS y) EvO oab = ?epno_so
evensPlusNotOdd (EvSS y) (EvSS z) oab = ?epno_ss
---------- Proofs ----------
Proof.proof31 = proof
intro a
intro b
intro ea
intro eb
induction ea
compute
exact eb
intro x
intro ex
intro exh
exact (EvSS exh)
Proof.proof33 = proof
intros
induction a
compute
rewrite sym (plus0_r b)
trivial
intro a'
intro ha'
compute
rewrite sym (plusS_r b a')
exact (congS ha')
Proof.epno_ss = proof
intro x
intro ex
intro y
intro ey
compute
rewrite sym ( plusS_r x (S y))
rewrite sym ( plusS_r x y)
intro os4xy
let es4xy = EvSS(EvSS (evensPlus1 ex ey))
exact evenNotOdd es4xy os4xy
Proof.epno_so = proof
intro x
intro ex
rewrite sym (plus0_r x)
compute
rewrite sym (plus0_r x)
intro ossx
exact evenNotOdd (EvSS ex) ossx
</lang>
=={{header|J}}==
| |||