[Agda] Some proofs by clauses

[James Wood]

It is not true. When you consider the case where y = true, we have that
f true false = 1 by the definition f true x = 1. f y false = 2 does not
hold definitionally because f true x = 1 has precedence.

To avoid this kind of definition, you can use the --exact-split option.
See
http://agda.readthedocs.io/en/latest/language/function-definitions.html#case-trees
.

James|
|

On 03/07/17 14:35, Manuel Bärenz wrote:
>
> I didn't try, but how about pattern match on y, for example in a
> with-clause? Then the proof should be refl.
>
>
> On 2017-07-03 15:34, v0id_NULL wrote:
>> Dear list,
>>
>> Help me please. How can I prove type of p2?
>>
>> module M1 where
>>
>> open import Data.Nat using (ℕ)
>> open import Data.Bool using (Bool; true; false)
>> open import Relation.Binary.PropositionalEquality using (_≡_; refl)
>>
>> f : Bool → Bool → ℕ
>> f true x = 1
>> f y false = 2
>> f false true = 3
>>
>> p1 : {x : Bool} → f true x ≡ 1
>> p1 = refl
>>
>> p2 : {y : Bool} → f y false ≡ 2
>> p2 = {!!}
>>
>> p3 : f false true ≡ 3
>> p3 = refl
>>
>>
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170703/ace44650/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170703/ace44650/attachment.sig>