Closed MarcelineVQ closed 5 years ago
Thanks! After a quick glance, this looks good to me. I think a PR would be great. We can always continue to improve later, but this would be an improvement already.
I've gone through and finished the section, below is what's required to do all the unit tests. My question about this before making a PR based on it is: Note that only some of the tests require supplying f and x. Should I have f and x in all of them for consistency or just include them where required? I'm not quite sure why some need it and some don't.
Church was only used where required because I plan to explain why it is this way.
namespace Church {
Nat' : {x : Type} -> Type
Nat' {x} = (x -> x) -> x -> x
one : Nat'
one f x = f x
two : Nat'
two f x = f (f x)
three : Nat'
three f x = f (f (f x))
zero : Nat'
zero f x = x
succ' : (n : Nat' {x}) -> Nat' {x}
succ' n = \f, x => f (n f x)
succ'_1 : succ' Church.zero f x = one f x
succ'_1 = Refl
succ'_2 : succ' Church.one f x = two f x
succ'_2 = Refl
succ'_3 : succ' Church.two f x = three f x
succ'_3 = Refl
plus' : (n, m : Nat' {x}) -> Nat' {x}
plus' n m = \f, x => n f (m f x)
plus'_1 : plus' Church.zero Church.one f x = one f x
plus'_1 = Refl
plus'_2 : plus' Church.two Church.three = plus' Church.three Church.two
plus'_2 = Refl
plus'_3 : plus' (plus' Church.two Church.two) Church.three = plus' Church.one (plus' Church.three Church.three)
plus'_3 = Refl
mult' : (n, m : Nat' {x}) -> Nat' {x}
mult' n m = \f, x => m (n f) x
mult'_1 : mult' Church.one Church.one f x = one f x
mult'_1 = Refl
mult'_2 : mult' Church.zero (plus' Church.three Church.three) f x = zero f x
mult'_2 = Refl
mult'_3 : mult' Church.two Church.three = plus' Church.three Church.three
mult'_3 = Refl
exp' : (n : Nat' {x}) -> (m : Nat' {x = x -> x}) -> Nat' {x}
exp' n m = \f, x => m n f x
exp'_1 : exp' Church.two Church.two = plus' Church.two Church.two
exp'_1 = Refl
exp'_2 : exp' Church.three Church.two = plus' (mult' Church.two (mult' Church.two Church.two)) Church.one
exp'_2 = Refl
exp'_3 : exp' Church.three Church.zero f x = one f x
exp'_3 = Refl
}
I'd say you should make a judgment call, but personally I'd lean toward only supplying f
and x
when required.
Poly.lidr note of: https://github.com/idris-hackers/software-foundations/blob/develop/src/Poly.lidr#L1027
Can be solved written as:
Omitting f, x, or Church will cause issues. Having to provide f and x seems necessary to collapse the lambdas, if that wording makes sense at all. Having to provide Church is part of a problem Idris seems to have in deciding whether something lowercase is an identifier from elsewhere or a fresh type variable.
This isn't a PR since I'm not 100% on what is considered good style yet but I wanted to share that there is a solution.