coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Axioms of parametricity?

From: Taral <taralx AT gmail.com>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] Axioms of parametricity?
Date: Tue, 18 Nov 2008 14:49:31 -0800
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=message-id:date:from:to:subject:mime-version:content-type :content-transfer-encoding:content-disposition; b=FLHwyN6QFSWkGjMZaClI/otOKz7HLBxhw4Eq5qxVn3uGcd6ocPNXigaAal/ueuakz2 K+HOYA022w4wNSbE0KxFNTalqgYFOcdS9B6kF2sW+Oi9IP8KbVXHDSAqpar7KjJPpC3F CAl/ucJheqxTvaDCuxWvJRux0G+p2HscPgCfo=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

I need this somehow:

Variable var : Type.

Inductive test : Type :=
| A : var -> test
| B : test.

Goal forall T (f : T -> test) x y v, f x = A v -> exists v', f y = A v'.

Any ideas? Impossible?

--
Taral
<taralx AT gmail.com>
"Please let me know if there's any further trouble I can give you."
-- Unknown

[Coq-Club] Axioms of parametricity?, Taral
- Re: [Coq-Club] Axioms of parametricity?, Andr� Hirschowitz
  - Re: [Coq-Club] Axioms of parametricity?, Taral
    - Re: [Coq-Club] Axioms of parametricity?, Matthew Brecknell
      - Re: [Coq-Club] Axioms of parametricity?, Taral
    - Re: [Coq-Club] Axioms of parametricity?, JAEGER, Eric (SGDN)
      - Re: [Coq-Club] Axioms of parametricity?, Yves Bertot
        
        Re: [Coq-Club] Axioms of parametricity?, Matthieu Sozeau
        
        Re: [Coq-Club] Axioms of parametricity?, Taral