[Agda] Komencenta demando.

[Andreas Abel]

On 06.12.2015 00:21, Serge Leblanc wrote:
>
> Why the system don't understand that (conv⁰← (conv⁰→ n)) is identity
> function when i writing this:
> proof¹′ (2k n) .(conv⁰→ n + conv⁰→ n) refl = cong 2k (proof¹′ n (conv⁰→
> n) refl)

It, does, but this does not prove the goal:

Goal: conv⁰← (conv⁰→ n + conv⁰→ n) ≡ 2k n
Have: 2k (conv⁰← (conv⁰→ n)) ≡ 2k n

> in this proof :
>
>
> proof¹′ : ∀ n m → m ≡ conv⁰→ n → conv⁰← m ≡ nf
> proof¹′ zero .0 refl = refl
> proof¹′ (2k n) .(conv⁰→ n + conv⁰→ n) refl = cong 2k (proof¹′ n (conv⁰→
> n) refl)
> proof¹′ (2k+1 n) .(suc (conv⁰→ n + conv⁰→ n)) refl = begin
>    conv⁰← (conv⁰→ (2k+1 n)) ≡[ refl ]
>    conv⁰← (conv⁰→ (suc⁰ (2k n))) ≡[ refl ]
>    conv⁰← (suc (conv⁰→ (2k n))) ≡[ refl ]
>    suc⁰ (conv⁰← (conv⁰→ (2k n))) ≡[ cong suc⁰ (proof¹′ (2k n) (conv⁰→ n
> + conv⁰→ n) refl) ]
>    suc⁰ (2k n) ≡[ refl ]
>    2k+1 n
>    ∎
>
> Sinceran dankon pro via helpo !
>
>
> On 2015-12-02 20:16, Andreas Abel wrote:
>> You can try to help the termination checker by proving the
>> superficially more general
>>
>> proof¹′ : ∀ n m → m ≡ conv⁰→ n → conv⁰← m ≡ n
>> proof¹′ zero .0 refl = refl
>> proof¹′ (2k n) m p = {!!}
>> proof¹′ (2k+1 n) .(suc (conv⁰→ n + conv⁰→ n)) refl = begin
>>   conv⁰← (conv⁰→ (2k+1 n)) ≡[ refl ]
>>   conv⁰← (conv⁰→ (suc⁰ (2k n))) ≡[ refl ]
>>   conv⁰← (suc (conv⁰→ (2k n))) ≡[ refl ]
>>   suc⁰ (conv⁰← (conv⁰→ (2k n))) ≡[ cong suc⁰ (proof¹′ (2k n) (conv⁰→ n
>> + conv⁰→ n) refl) ]
>>   suc⁰ (2k n) ≡[ refl ]
>>   2k+1 n
>>   ∎
>>
>> and then get your final result by
>>
>> proof¹ : ∀ n → conv⁰← (conv⁰→ n) ≡ n
>> proof¹ n = proof¹′ n (conv⁰→ n) refl
>>
>> I did not complete the hole you left, so I do not know whether it
>> works in the end...
>>
>> The idea is that Agda can now also use the descent on m, in this case,
>>
>>   (suc (conv⁰→ n + conv⁰→ n)) > (conv⁰→ n + conv⁰→ n)
>>
>> to convince herself of termination.
>>
>> Cheers,
>> Andreas
>>
>> On 01.12.2015 22:13, Serge Leblanc wrote:
>>> open import Data.Nat
>>> open import Data.Nat.Properties.Simple using (+-comm; +-suc)
>>> open import Relation.Binary.PropositionalEquality as PropEq using (_≡_;
>>> refl; cong; cong₂)
>>> open PropEq.≡-Reasoning renaming (_≡⟨_⟩_ to _≡[_]_)
>>>
>>> data ℕ⁰ : Set where
>>>    zero : ℕ⁰
>>>    2k : ℕ⁰ → ℕ⁰
>>>    2k+1 : ℕ⁰ → ℕ⁰
>>>
>>> suc⁰ : ℕ⁰ → ℕ⁰
>>> suc⁰ zero = 2k+1 zero
>>> suc⁰ (2k n) = 2k+1 n
>>> suc⁰ (2k+1 n) = 2k (suc⁰ n)
>>>
>>> conv⁰→ : ℕ⁰ → ℕ
>>> conv⁰→ zero = zero
>>> conv⁰→ (2k n) = conv⁰→ n + conv⁰→ n
>>> conv⁰→ (2k+1 n) = suc (conv⁰→ n + conv⁰→ n)
>>>
>>> conv⁰← : ℕ → ℕ⁰
>>> conv⁰← zero = zero
>>> conv⁰← (suc n) = suc⁰ (conv⁰← n)
>>>
>>> suc-conv : (n : ℕ⁰) → conv⁰→ (suc⁰ n) ≡ suc (conv⁰→ n)
>>> suc-conv zero = refl
>>> suc-conv (2k n) = refl
>>> suc-conv (2k+1 n) = begin
>>>                      conv⁰→ (suc⁰ (2k+1 n)) ≡[ refl ]
>>>                      conv⁰→ (2k (suc⁰ n)) ≡[ refl ]
>>>                      conv⁰→ (suc⁰ n) + conv⁰→ (suc⁰ n) ≡[ cong₂ _+_
>>> (suc-conv
>>> n) (suc-conv n) ]
>>>                      suc (conv⁰→ n) + suc (conv⁰→ n) ≡[ cong suc (+-suc
>>> (conv⁰→ n) (conv⁰→ n)) ]
>>>                      suc (suc (conv⁰→ n + conv⁰→ n)) ≡[ refl ]
>>>                      suc (conv⁰→ (2k+1 n))
>>>                      ∎
>>>
>>> proof⁰ : ∀ n → conv⁰→ (conv⁰← n) ≡ n
>>> proof⁰ zero = refl
>>> proof⁰ (suc n) = begin
>>>                   conv⁰→ (conv⁰← (suc n)) ≡[ refl ]
>>>                   conv⁰→ (suc⁰ (conv⁰← n)) ≡[ suc-conv (conv⁰← n) ]
>>>                   suc (conv⁰→ (conv⁰← n)) ≡[ cong suc (proof⁰ n) ]
>>>                   suc n
>>>                   ∎
>>>
>>> proof¹ : ∀ n → conv⁰← (conv⁰→ n) ≡ n
>>> proof¹ zero = refl
>>> proof¹ (2k n) = {! !}
>>> proof¹ (2k+1 n) = begin
>>>    conv⁰← (conv⁰→ (2k+1 n)) ≡[ refl ]
>>>    conv⁰← (conv⁰→ (suc⁰ (2k n))) ≡[ refl ]
>>>    conv⁰← (suc (conv⁰→ (2k n))) ≡[ refl ]
>>>    suc⁰ (conv⁰← (conv⁰→ (2k n))) ≡[ cong suc⁰ (proof¹ (2k n)) ]
>>>    suc⁰ (2k n) ≡[ refl ]
>>>    2k+1 n
>>>    ∎
>>
>>
>
> --
> Serge Leblanc
> ------------------------------------------------------------------------
> gpg --keyserver hkp://keyserver.ubuntu.com:11371 --recv-keys 0x67B17A3F
> Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/