Simplify and add Nat proofs

[nickdrozd]

Simplify some existing Nat proofs, then port over some proofs from Idris 1.

Some of the added proofs go through in Idris 1, but not Idris 2. Those proofs are commented out here, and they should be considered bugs.

[nickdrozd]

Looks like a test failure:

idris2/reflection003: FAILURE
Expected:
"1/1: Building refprims (refprims.idr)\nLOG 0: Name: Prelude.List.++\nLOG 0: Type: (%pi Rig0 Implicit Just a %type (%pi Rig1 Explicit Just _ (Prelude.List a) (%pi RigW Explicit Nothing (Prelude.List a) (Prelude.List a))))\nLOG 0: Name: Prelude.Strings.++\nLOG 0: Type: (%pi Rig1 Explicit Just _ String (%pi Rig1 Explicit Just _ String String))\nLOG 0: Resolved name: Prelude.Nat\nLOG 0: Constructors: [Prelude.Z, Prelude.S]\nrefprims.idr:37:10--39:1:While processing right hand side of dummy1 at refprims.idr:37:1--39:1:\nError during reflection: Not really trying\nrefprims.idr:40:10--42:1:While processing right hand side of dummy2 at refprims.idr:40:1--42:1:\nError during reflection: Still not trying\nrefprims.idr:43:10--45:1:While processing right hand side of dummy3 at refprims.idr:43:1--45:1:\nError during reflection: Undefined name\nrefprims.idr:46:10--48:1:While processing right hand side of dummy4 at refprims.idr:46:1--48:1:\nError during reflection: failed after generating Main.{plus:5841}\n"
Given:
"1/1: Building refprims (refprims.idr)\nLOG 0: Name: Prelude.List.++\nLOG 0: Type: (%pi Rig0 Implicit Just a %type (%pi Rig1 Explicit Just _ (Prelude.List a) (%pi RigW Explicit Nothing (Prelude.List a) (Prelude.List a))))\nLOG 0: Name: Prelude.Strings.++\nLOG 0: Type: (%pi Rig1 Explicit Just _ String (%pi Rig1 Explicit Just _ String String))\nLOG 0: Resolved name: Prelude.Nat\nLOG 0: Constructors: [Prelude.Z, Prelude.S]\nrefprims.idr:37:10--39:1:While processing right hand side of dummy1 at refprims.idr:37:1--39:1:\nError during reflection: Not really trying\nrefprims.idr:40:10--42:1:While processing right hand side of dummy2 at refprims.idr:40:1--42:1:\nError during reflection: Still not trying\nrefprims.idr:43:10--45:1:While processing right hand side of dummy3 at refprims.idr:43:1--45:1:\nError during reflection: Undefined name\nrefprims.idr:46:10--48:1:While processing right hand side of dummy4 at refprims.idr:46:1--48:1:\nError during reflection: failed after generating Main.{plus:6081}\n"

I'm not sure what that means.

[edwinb]

If you update the prelude some of the internal names will change, and the reflection mechanism will expose that. So this is fine, you just need to update the test output. "make test" will let you do that interactively.

[edwinb]

Of course I resolved the conflict wrongly, didn't I... I will fix it.

[nickdrozd]

@edwinb FYI, this one contained unimplemented theorems. As with #242, their proofs go through in Idris 1 but not 2. So master now has some uncontroversial but nevertheless unproved statements. Then again, they do serve as convenient test cases for any proposed fixes.