[Agda] Re: [Coq-Club] Propositional extensionality: the return of the revenge

[Maxime Dénès]

Oh, thanks Andreas! I was curious to know if this paradox could be 
ported, but didn't know enough about co-induction in Agda.

It seems to indicate that this is more than just an implementation bug. 
Which is not surprising after all, it is the dual of the original 
problem with fixpoints on inductive types.

A minor point, I think you can get rid of CoFalse. I had introduced it 
in the original Coq example because of an implementation detail (bug?) 
of the guard checker, which by accident almost prevented the paradox, 
but not quite :)

prop = Set

data False : prop where

data Pandora : prop where
   C : ∞ False → Pandora

postulate
   ext : (False → Pandora) → (Pandora → False) → False ≡ Pandora

foo : False ≡ Pandora
foo = ext (λ{ ()               })
           (λ{ (C c) → (♭ c)})

loop : False
loop rewrite foo = C (♯ loop)

Maxime.

On 03/02/2014 02:07 PM, Andreas Abel wrote:
> Here is the Agda version of this paradox:
>
> open import Common.Coinduction
> open import Common.Equality
>
> prop = Set
>
> data False : prop where
>
> data CoFalse : prop where
>   CF : False → CoFalse
>
> data Pandora : prop where
>   C : ∞ CoFalse → Pandora
>
> postulate
>   ext : (CoFalse → Pandora) → (Pandora → CoFalse) → CoFalse ≡ Pandora
>
> out : CoFalse → False
> out (CF f) = f
>
> foo : CoFalse ≡ Pandora
> foo = ext (λ{ (CF ())               })
>           (λ{ (C c) → CF (out (♭ c))})
>
> loop : CoFalse
> loop rewrite foo = C (♯ loop)
>
> false : False
> false = out loop
>
> This concerns the current "musical" coinduction mechanism (which was 
> never sound anyway).
>
> I could not reproduce it with copatterns, since with and rewrite are 
> not implemented for copatterns and a use of subst destroys 
> guardedness.  (I will think twice how I implement it now... ;-)).
>
> Cheers,
> Andreas
>
>
> On 27.02.2014 06:12, Jason Gross wrote:
>> I thought that your extra CoFalse argument to CF was redundant, so I
>> tried removing it.  Then I got
>>
>> Error:
>> Recursive definition of loop is ill-formed.
>> In environment
>> loop : CoFalse
>> Recursive call on a non-recursive argument of constructor
>> "loop".
>> Recursive definition is:
>> "match foo in (_ = T) return T with
>>   | eq_refl => C loop
>>   end".
>>
>>
>> What does this mean?  Does Coq somehow think that "loop" is a
>> constructor?  And why is whether or not "loop" is valid for a recursive
>> call dependent on whether or not there's a dummy CoFalse hypothesis 
>> of CF?
>>
>> -Jason
>>
>>
>> On Wed, Feb 26, 2014 at 11:56 PM, Maxime Dénès <mail at maximedenes.fr
>> <mailto:mail at maximedenes.fr>> wrote:
>>
>>     Hello there,
>>
>>     As some of you may have been expecting, episode two is out. This
>>     time featuring co-inductive types!
>>
>> ------------------------------__------------------------------__---------------------
>>     CoInductive CoFalse : Prop := CF : CoFalse -> False -> CoFalse.
>>
>>     CoInductive Pandora : Prop := C : CoFalse -> Pandora.
>>
>>     Axiom prop_ext : forall P Q : Prop, (P<->Q) -> P = Q.
>>
>>     Lemma foo : Pandora = CoFalse.
>>     apply prop_ext.
>>     constructor.
>>     intro x; destruct x; assumption.
>>     exact C.
>>     Qed.
>>
>>     CoFixpoint loop : CoFalse :=
>>     match foo in (_ = T) return T with eq_refl => C loop end.
>>
>>     Definition ff : False := match loop with CF _ t => t end.
>> ------------------------------__------------------------------__---------------------
>>
>>     I am still not sure if this is an implementation bug of the guard
>>     for cofixpoints or something more fundamental.
>>
>>     Below is a variation done with Arthur Azevedo de Amorim (requires
>>     some of the definitions above):
>>
>> ------------------------------__------------------------------__---------------------
>>     Inductive omega := Omega : omega -> omega.
>>
>>     Lemma H : omega = CoFalse.
>>     Proof.
>>     apply prop_ext; constructor.
>>        induction 1; assumption.
>>     destruct 1; destruct H0.
>>     Qed.
>>
>>     CoFixpoint loop' : CoFalse :=
>>        match H in _ = T return T with
>>          eq_refl =>
>>          Omega match eq_sym H in _ = T return T with eq_refl => loop' 
>> end
>>        end.
>>
>>     Definition ff' : False := match loop' with CF _ t => t end.
>> ------------------------------__------------------------------__---------------------
>>
>>     We'll work on a fix before the next Coq release.
>>
>>     Maxime.
>>
>>
>
>