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

[Andreas Abel]

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.
>
>


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

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

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