Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Generalizing dependently typed functions

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Generalizing dependently typed functions


Chronological Thread 
  • 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
*)



Archive powered by MHonArc 2.6.18.

Top of Page