Two example on this page:
- plusReducesZ
- Plus Commutes
plusReducesZ
| First I created a file 'plusReducesZ.idr' containing the following: | import Pruviloj
import Pruviloj.Induction
plusReducesZ' : (n:Nat) -> n = plus n Z
plusReducesZ' Z = ?plusredZ_Z
plusReducesZ' (S k) = let ih = plusReducesZ' k in
?plusredZ_S |
Then run Idris using this file:
| Start Idris | mjb@linux:~> cd Idris-dev2/libs/algebra
mjb@linux:~/Idris-dev2/libs/algebra> idris plusReducesZ.idr -p pruviloj
/ _/___/ /____(_)____
/ // __ / ___/ / ___/ Version 1.2.0
_/ // /_/ / / / (__ ) http://www.idris-lang.org/
/___/\__,_/_/ /_/____/ Type :? for help
Idris is free software with ABSOLUTELY NO WARRANTY.
For details type :warranty.
Holes: Main.plusredZ_S, Main.plusredZ_Z |
*plusReducesZ> :module Language.Reflection.Elab Holes: Main.plusredZ_S, Main.plusredZ_Z |
|
| Start Elab | *plusReducesZ> :elab plusredZ_Z
---------- Goal: ----------
{hole_0} : 0 = 0 |
use reflexivity from pruviloj library this solves plusReducesZ |
-Main.plusredZ_Z> reflexivity plusredZ_Z: No more goals. -Main.plusredZ_Z> :qed Proof completed! Main.plusredZ_Z = %runElab (do reflexivity) Holes: Main.plusredZ_S *plusReducesZ> |
| now solve plusredZ_S | *plusReducesZ> :elab plusredZ_S
---------- Goal: ----------
{hole_0} : (k : Nat) -> (k = plus k 0) -> S k = S (plus k 0)
-Main.plusredZ_S> intro `{{k}}
---------- Assumptions: ----------
k : Nat
---------- Goal: ----------
{hole_0} : (k = plus k 0) -> S k = S (plus k 0)
-Main.plusredZ_S> intro `{{ih}}
---------- Assumptions: ----------
k : Nat
ih : k = plus k 0
---------- Goal: ----------
{hole_0} : S k = S (plus k 0)
-Main.plusredZ_S> compute
---------- Assumptions: ----------
k : Nat
ih : k = plus k 0
---------- Goal: ----------
{hole_0} : S k = S (plus k 0)
-Main.plusredZ_S> rewriteWith (Var `{{ih}})
---------- Assumptions: ----------
k : Nat
ih : k = plus k 0
---------- Goal: ----------
{hole_0} : S k = S k
-Main.plusredZ_S> reflexivity
plusredZ_S: No more goals.
-Main.plusredZ_S> :qed
Proof completed!
Main.plusredZ_S = %runElab (do intro `{{k}}
intro `{{ih}}
compute
rewriteWith (Var `{{ih}})
reflexivity)
*plusReducesZ> |
Plus Commutes
| First I created a file 'plusCom.idr' containing the following: | import Pruviloj import Pruviloj.Induction plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n plus_commutes n m = ?plus_commutes_rhs |
| try to adapt Coq proof here | Theorem plus_sym: (forall n m, n + m = m + n).
Proof.
intros n m.
elim n.
base case for n
elim m.
base case for m
exact (eq_refl (O + O)).
inductive case for m
intros m'.
intros inductive_hyp_m.
simpl.
rewrite <- inductive_hyp_m.
simpl.
exact (eq_refl (S m')).
inductive case for n
intros n'.
intros inductive_hyp_n.
simpl.
rewrite inductive_hyp_n.
elim m.
base case for m
simpl.
exact (eq_refl (S n')).
intros m'.
intros inductive_hyp_m.
simpl.
rewrite inductive_hyp_m.
simpl.
exact (eq_refl (S (m' + S n'))).
Qed. |
Then run Idris using this file:
| Start Idris | mjb@linux:~> cd Idris-dev2/libs/algebra
mjb@linux:~/Idris-dev2/libs/algebra> idris plusCom.idr -p pruviloj
____ __ _
/ _/___/ /____(_)____
/ // __ / ___/ / ___/ Version 1.2.0
_/ // /_/ / / / (__ ) http://www.idris-lang.org/
/___/\__,_/_/ /_/____/ Type :? for help
Idris is free software with ABSOLUTELY NO WARRANTY.
For details type :warranty.
Holes: Main.plus_commutes_rhs |
*identity> :module Language.Reflection.Elab Holes: Main.plus_commutes_rhs |
|
| Start Elab | *identity> :elab plus_commutes_rhs
---------- Goal: ----------
{hole_0} : (n : Nat) -> (m : Nat) -> plus n m = plus m n |
| Intro | -Main.plus_commutes_rhs> intro `{{n}}
---------- Assumptions: ----------
n : Nat
---------- Goal: ----------
{hole_0} : (m : Nat) -> plus n m = plus m n
-Main.plus_commutes_rhs> intro `{{m}}
---------- Assumptions: ----------
n : Nat
m : Nat
---------- Goal: ----------
{hole_0} : plus n m = plus m n
-Main.plus_commutes_rhs>
|
I'm stuck
Assoc
mjb@linux:~> cd Idris-dev2/libs/algebra
mjb@linux:~/Idris-dev2/libs/algebra> idris concatAssoc -p pruviloj
____ __ _
/ _/___/ /____(_)____
/ // __ / ___/ / ___/ Version 1.2.0
_/ // /_/ / / / (__ ) http://www.idris-lang.org/
/___/\__,_/_/ /_/____/ Type :? for help
Idris is free software with ABSOLUTELY NO WARRANTY.
For details type :warranty.
Type checking ./concatAssoc.idr
Holes: Main.hole
*concatAssoc> :module Language.Reflection.Elab
Holes: Main.hole
*concatAssoc> :elab hole
---------- Goal: ----------
{hole_0} : (a : Type) ->
(xs : List a) -> (ys : List a) -> (zs : List a) -> (xs ++ ys) ++ zs = xs ++ ys ++ zs
-Main.hole> intro `{{a}}
---------- Assumptions: ----------
a : Type
---------- Goal: ----------
{hole_0} : (xs : List a) ->
(ys : List a) -> (zs : List a) -> (xs ++ ys) ++ zs = xs ++ ys ++ zs
-Main.hole> intro `{{xs}}
---------- Assumptions: ----------
a : Type
xs : List a
---------- Goal: ----------
{hole_0} : (ys : List a) -> (zs : List a) -> (xs ++ ys) ++ zs = xs ++ ys ++ zs
-Main.hole> intro `{{ys}}
---------- Assumptions: ----------
a : Type
xs : List a
ys : List a
---------- Goal: ----------
{hole_0} : (zs : List a) -> (xs ++ ys) ++ zs = xs ++ ys ++ zs
-Main.hole> intro `{{zs}}
---------- Assumptions: ----------
a : Type
xs : List a
ys : List a
zs : List a
---------- Goal: ----------
{hole_0} : (xs ++ ys) ++ zs = xs ++ ys ++ zs
-Main.hole> induction (Var `{{xs}})
---------- Other goals: ----------
{::_154}
---------- Assumptions: ----------
a : Type
xs : List a
ys : List a
zs : List a
---------- Goal: ----------
{Nil_153} : (\subj => (subj ++ ys) ++ zs = subj ++ ys ++ zs) []
-Main.hole> compute
---------- Other goals: ----------
{::_154}
---------- Assumptions: ----------
a : Type
xs : List a
ys : List a
zs : List a
---------- Goal: ----------
{Nil_153} : ys ++ zs = ys ++ zs
-Main.hole> reflexivity
---------- Assumptions: ----------
a : Type
xs : List a
ys : List a
zs : List a
---------- Goal: ----------
{::_154} : (x : a) ->
(xs : List a) ->
(\subj => (subj ++ ys) ++ zs = subj ++ ys ++ zs) xs ->
(\subj => (subj ++ ys) ++ zs = subj ++ ys ++ zs) (x :: xs)
-Main.hole> compute
---------- Assumptions: ----------
a : Type
xs : List a
ys : List a
zs : List a
---------- Goal: ----------
{::_154} : (x : a) ->
(xs : List a) ->
((xs ++ ys) ++ zs = xs ++ ys ++ zs) -> x :: (xs ++ ys) ++ zs = x :: xs ++ ys ++ zs
-Main.hole> attack
---------- Other goals: ----------
{::_154}
---------- Assumptions: ----------
a : Type
xs : List a
ys : List a
zs : List a
---------- Goal: ----------
{hole_57} : (x : a) ->
(xs : List a) ->
((xs ++ ys) ++ zs = xs ++ ys ++ zs) -> x :: (xs ++ ys) ++ zs = x :: xs ++ ys ++ zs
-Main.hole> intro `{{x}}
---------- Other goals: ----------
{::_154}
---------- Assumptions: ----------
a : Type
xs : List a
ys : List a
zs : List a
x : a
---------- Goal: ----------
{hole_57} : (xs : List a) ->
((xs ++ ys) ++ zs = xs ++ ys ++ zs) -> x :: (xs ++ ys) ++ zs = x :: xs ++ ys ++ zs
-Main.hole> intro `{{xs'}}
---------- Other goals: ----------
{::_154}
---------- Assumptions: ----------
a : Type
xs : List a
ys : List a
zs : List a
x : a
xs' : List a
---------- Goal: ----------
{hole_57} : ((xs' ++ ys) ++ zs = xs' ++ ys ++ zs) ->
x :: (xs' ++ ys) ++ zs = x :: xs' ++ ys ++ zs
-Main.hole> intro `{{IH}}
---------- Other goals: ----------
{::_154}
---------- Assumptions: ----------
a : Type
xs : List a
ys : List a
zs : List a
x : a
xs' : List a
IH : (xs' ++ ys) ++ zs = xs' ++ ys ++ zs
---------- Goal: ----------
{hole_57} : x :: (xs' ++ ys) ++ zs = x :: xs' ++ ys ++ zs
-Main.hole> rewriteWith (Var `{{IH}})
---------- Other goals: ----------
{::_154}
---------- Assumptions: ----------
a : Type
xs : List a
ys : List a
zs : List a
x : a
xs' : List a
IH : (xs' ++ ys) ++ zs = xs' ++ ys ++ zs
---------- Goal: ----------
{hole_57} : x :: (xs' ++ ys) ++ zs = x :: (xs' ++ ys) ++ zs
-Main.hole> reflexivity
---------- Assumptions: ----------
a : Type
xs : List a
ys : List a
zs : List a
---------- Goal: ----------
{::_154} : (x : a) ->
(xs : List a) ->
((xs ++ ys) ++ zs = xs ++ ys ++ zs) ->
x :: (xs ++ ys) ++ zs = x :: xs ++ ys ++ zs =?= \x, xs', IH => replace IH Refl
-Main.hole> solve
hole: No more goals.
-Main.hole> :qed
Proof completed!
Main.hole = %runElab (do intro `{{a}}
intro `{{xs}}
intro `{{ys}}
intro `{{zs}}
induction (Var `{{xs}})
compute
reflexivity
compute
attack
intro `{{x}}
intro `{{xs'}}
intro `{{IH}}
rewriteWith (Var `{{IH}})
reflexivity
solve)
*concatAssoc>
|
