coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Robbert Krebbers <mailinglists AT robbertkrebbers.nl>
- To: Jason Gross <jasongross9 AT gmail.com>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Generalizing dependently typed functions
- Date: Tue, 29 May 2012 09:39:46 +0200
Keep in mind that in your example dependent destruction silently assumes the JMeq_eq axiom.
However, I do not know whether it can be proven without.
On 05/29/2012 04:19 AM, Jason Gross wrote:
I discovered that replacing "intros []" with "intro r; dependent
destruction r" fixes things, if I [Require Import Program].
Require Import Program.
Parameter f : forall T (a : Type), T a a -> Prop.
Implicit Arguments f [T a].
Inductive g T (a : Type) : forall (b : Type) (x : T a b), Prop :=
| injf : forall (t : T a a), f t -> g T a a t.
Implicit Arguments g [T a b].
Theorem g_ne T (a b : Type) (x : T a b) : a <> b -> ~g x.
intros H gx ; inversion gx ; contradiction.
Qed.
Theorem f_eq_g T (a : Type) (x : T a a) : f x <-> g x.
split.
intro fx ; constructor ; assumption.
intro r; now dependent destruction r.
Qed.
Print Assumptions f_eq_g.
(*
Axioms:
JMeq_eq : forall (A : Type) (x y : A), x ~= y -> x = y
f : forall (T : Type -> Type -> Type) (a : Type), T a a -> Prop
*)
- [Coq-Club] Generalizing dependently typed functions, Jason Gross, 05/28/2012
- Re: [Coq-Club] Generalizing dependently typed functions, gallais @ ensl.org, 05/28/2012
- Re: [Coq-Club] Generalizing dependently typed functions, Jason Gross, 05/29/2012
- Re: [Coq-Club] Generalizing dependently typed functions, Jason Gross, 05/29/2012
- Re: [Coq-Club] Generalizing dependently typed functions, Robbert Krebbers, 05/29/2012
- Re: [Coq-Club] Generalizing dependently typed functions, Jason Gross, 05/29/2012
- Re: [Coq-Club] Generalizing dependently typed functions, Jason Gross, 05/29/2012
- Re: [Coq-Club] Generalizing dependently typed functions, gallais @ ensl.org, 05/28/2012
Archive powered by MHonArc 2.6.18.