# Natural Number Example - Elaborator Reflection

• 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

see

 ```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> ```