-
-
Save aymanosman/9db1db11755ef4b4759c4ee9a4bdb515 to your computer and use it in GitHub Desktop.
| #lang pie | |
| (claim > | |
| (-> Nat Nat Nat)) | |
| (define > | |
| (lambda (n) | |
| (rec-Nat n | |
| (the (-> Nat Nat) (lambda (m) 0)) | |
| (lambda (n-1 n-1>) | |
| (lambda (m) | |
| (rec-Nat m | |
| 1 | |
| (lambda (m-1 _) | |
| (n-1> m-1)))))))) | |
| (claim max | |
| (-> Nat Nat Nat)) | |
| (define max | |
| (lambda (n m) | |
| (rec-Nat (> n m) | |
| m | |
| (lambda (_ _) n)))) | |
| (check-same Nat 0 (max 0 0)) | |
| (check-same Nat 1 (max 1 0)) | |
| (check-same Nat 1 (max 0 1)) | |
| (check-same Nat 2 (max 2 1)) | |
| (check-same Nat 2 (max 1 2)) |
Cool!
Factoring out add1 is neat.
We learnt early on whilst studying The Little Typer that introducing too many variables at the start often caused problems.
My mathematician friend tells me it has something to do with "making the inductive hypothesis too weak". I can't say I have fully understood what that means, but what I can tell you is that by introducing fewer variables at the start you can let the later variables vary with respect to the earlier and make the inductive hypothesis you obtain more flexible and thus more useful.
Although the above example does not use ind-Nat, I think something similar is happening.
I think it is impossible to define this function by introducing both n and m.
Hope that helps.
I agree. I too suspect that it's not possible to introduce m at the start . For what it's worth it seems similar to an issue I encountered when using another dependently typed language called Lean, and a tactic called revert. You can read a discussion of it on the Lean Zulip archive (my contribution to the discussion was to observe that "I also found the use of revert ... tricky").
Thanks for the pointers.
You may be interested in this group https://www.meetup.com/London-TyDD, if you are based in London.
Nice! Below is a minor rewrite of your direct solution (which merely uses
which-Natand factors outadd1). What I was not able to do is introducemfrom the start (i.e.,(define max3 (λ(n m) TODO))); I would be interested in knowing whether it's possible.(claim id-Nat (-> Nat Nat)) (define id-Nat (λ(n) n)) (claim max3 (-> Nat Nat Nat)) (define max3 (λ(n) (rec-Nat n id-Nat (λ(n-1 f m) (add1 (which-Nat m n-1 f))))))