[Agda] a tutorial for proof by coinduction

[Guillaume Allais]

Hi Pierre,

Note that if you use copatterns to define the trees in BT' just like
you did for BT then the termination checker is perfectly happy:

====================================================================
mutual
  spine' : BT' ℕ
  node spine' = inj₂ (spine'' , record{node = inj₁ 0})
  spine'' : BT' ℕ
  spine'' = record {node = inj₂ (spine' , record{node = inj₁ 0})}

spine₀ : BT' ℕ
node spine₀ = inj₂ (spine₀ , record{node = inj₁ 0})
====================================================================

My guess is that the copattern version is accepted because copatterns
prevent eager unfolding. In comparison, a definition with a mere `record {}`
expression on the RHS is open to things being unfolded forever.

Cheers,
gallais


On 14/01/2020 11:21, Pierre Lescanne (en) wrote:
> I have a specific question.  Here are two formalisations of coinductive binary
> trees
> 
> mutual
>   record BT (A : Set) : Set where
>     coinductive
>     field
>       u : A ⊎ Node A
>         record Node (A : Set) : Set where
>     coinductive
>     field
>       ↙ ↘ : BT A
> 
> record BT' (A : Set) : Set where
>   coinductive
>   field
>     node : A ⊎ (BT' A × BT' A )
> 
> open BT
> open Node
> open BT'
> 
> -------------
> Now I define three objects/spine/  : one is in BT and two are in BT'.  Those in
> BT' are not accepted, I suspect that this is due to the termination checker,
> which prefers/record/  over/product/.
> Am I right ? Or am I mistaking ?
> -------------
> 
> mutual
>   spine : BT ℕ
>   spine = record {u = inj₂ spineN}
>     spineN : Node ℕ
>   ↙ spineN = spine
>   ↘ spineN = record{u = inj₁ 0}
> 
> mutual
>   spine' : BT' ℕ
>   spine' = record {node = inj₂ (spine'' , record{node = inj₁ 0})}
>     spine'' : BT' ℕ
>   spine'' = record {node = inj₂ (spine' , record{node = inj₁ 0})}
> 
> spine₀ : BT' ℕ
> spine₀ = record {node = inj₂ (spine₀ , record{node = inj₁ 0})}
> 
> 
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>