Natural Number Example - Elaborator Reflection

Two example on this page:

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> 

 

 


metadata block
see also:
Correspondence about this page

This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2022 Martin John Baker - All rights reserved - privacy policy.