Quelle bug_3209.v Sprache: Coq

(* Avoiding some occur-check *)

(* 1. Original example *)

Inductive eqT {A} (x : A) : A -> Type :=
  reflT : eqT x x.
Definition Bi_inv (A B : Type) (f : (A -> B)) :=
  sigT (fun (g : B -> A) =>
          sigT (fun (h : B -> A) =>
                  sigT (fun (α : forall b : B, eqT (f (g b)) b) =>
                          forall a : A, eqT (h (f a)) a))).
Definition TEquiv (A B : Type) := sigT (fun (f : A -> B) => Bi_inv _ _ f).

Axiom UA : forall (A B : Type), TEquiv (TEquiv A B) (eqT A B).
Definition idtoeqv {A B} (e : eqT A B) : TEquiv A B :=
  sigT_rect (fun _ => TEquiv A B)
            (fun (f : TEquiv A B -> eqT A B) H =>
               sigT_rect _ (* (fun _ => TEquiv A B) *)
                         (fun g _ => g e)
                         H)
            (UA A B).

(* 2. Alternative example by Guillaume *)

Inductive foo (A : Prop) : Prop := Foo : foo A.
Axiom bar : forall (A : Prop) (P : foo A -> Prop), (A -> P (Foo A)) -> Prop.

(* This used to fail with a Not_found, we fail more graciously but a
   heuristic could be implemented, e.g. in some smart occur-check
   function, to find a solution of then form ?P := fun _ => ?P' *)

Fail Check (fun e : ?[T] => bar ?[A] ?[P] (fun g : ?[A'] => g e)).

(* This works and tells which solution we could have inferred *)

Check (fun e : ?[T] => bar ?[A] (fun _ => ?[P]) (fun g : ?[A'] => g e)).

(* For the record, here is the trace in the failing example:

In (fun e : ?T => bar ?[A] ?[P] (fun g : ?A' => g e)), we have the existential variables

e:?T |- ?A : Prop
e:?T |- ?P : foo ?A -> Prop
e:?T |- ?A' : Type

with constraints

?A' == ?A
?A' == ?T -> ?P (Foo ?A)

To type (g e), unification first defines

?A := forall x:?B, ?P'{e:=e,x:=x}
with ?T <= ?B
and ?P'@{e:=e,x:=e} <= ?P@{e:=e} (Foo (forall x:?B, ?P'{e:=e,x:=x}))

Then, since ?P'@{e:=e,x:=e} may use "e" in two different ways, it is
not a pattern and we define a new

e:?T x:?B|- ?P'' : foo (?B' -> ?P''') -> Prop

for some ?B' and ?P''', together with

?P'@{e,x} := ?P''{e:=e,x:=e} (Foo (?B -> ?P')
?P@{e} := ?P''{e:=e,x:=e}

Moreover, ?B' and ?P''' have to satisfy

?B'@{e:=e,x:=e} == ?B@{e:=e}
?P'''@{e:=e,x:=e} == ?P'@{e:=e,x:=x}

and this leads to define ?P' which was the initial existential
variable to define.
*)

quality100%

¤ Dauer der Verarbeitung: 0.6 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.