SSL unification.v Sprache: Coq

#[local] Definition test_stack_unification_interaction_with_delta A
  : (if negb _ then true else false) = if orb false (negb A) then true else false
  := eq_refl.

(* Test patterns unification *)

Lemma l1 : (forall P, (exists x:nat, P x) -> False)
         -> forall P, (exists x:nat, P x /\ P x) -> False.
Proof.
intros; apply (H _ H0).
Qed.

Lemma l2 :  forall A:Set, forall Q:A->Set,
           (forall (P: forall x:A, Q x -> Prop),
                   (exists x:A, exists y:Q x, P x y) -> False)
         -> forall (P: forall x:A, Q x -> Prop),
                   (exists x:A, exists y:Q x, P x y /\ P x y) -> False.
Proof.
intros; apply (H _ H0).
Qed.

Lemma l3 : (forall P, ~(exists x:nat, P x))
         -> forall P:nat->Prop, ~(exists x:nat, P x -> P x).
Proof.
intros; apply H.
Qed.

  (* Feature introduced June 2011 *)

Lemma l7 : forall x (P:nat->Prop), (forall f, P (f x)) -> P (x+x).
Proof.
intros x P H; apply H.
Qed.

(* Example submitted for Zenon *)

Axiom zenon_noteq : forall T : Type, forall t : T, ((t <> t) -> False).
Axiom zenon_notall : forall T : Type, forall P : T -> Prop,
  (forall z : T, (~(P z) -> False)) -> (~(forall x : T, (P x)) -> False).

  (* Must infer "P := fun x => x=x" in zenon_notall *)
Check (fun _h1 => (zenon_notall nat _ (fun _T_0 =>
          (fun _h2 => (zenon_noteq _ _T_0 _h2))) _h1)).

(* Core of an example submitted by Ralph Matthes (BZ#849)

   It used to fail because of the K-variable x in the type of "sum_rec ..."
   which was not in the scope of the evar ?B. Solved by a head
   beta-reduction of the type "(fun _ : unit + unit => L unit) x" of
   "sum_rec ...". Shall we used more reduction when solving evars (in
   real_clean)?? Is there a risk of starting too long reductions?

   Note that the example originally came from a non re-typable
   pretty-printed term (the checked term is actually re-printed the
   same form it is checked).
*)

Set Implicit Arguments.
Inductive L (A:Set) : Set := c : A -> L A.
Parameter f: forall (A:Set)(B:Set), (A->B) -> L A -> L B.
Parameter t: L (unit + unit).

Check (f (fun x : unit + unit =>
  sum_rec (fun _ : unit + unit => L unit)
    (fun y => c y) (fun y => c y) x) t).

(* Test patterns unification in apply *)

Require Import TestSuite.arith.
Parameter x y : nat.
Parameter G:x=y->x=y->Prop.
Parameter K:x<>y->x<>y->Prop.
Lemma l4 : (forall f:x=y->Prop, forall g:x<>y->Prop,
            match eq_nat_dec x y with left a => f a | right a => g a end)
   -> match eq_nat_dec x y with left a => G a a | right a => K a a end.
Proof.
intros.
apply H.
Qed.

(* Test unification modulo eta-expansion (if possible) *)

(* In this example, two instances for ?P (argument of hypothesis H) can be
   inferred (one is by unifying the type [Q true] and [?P true] of the
   goal and type of [H]; the other is by unifying the argument of [f]);
   we need to unify both instances up to allowed eta-expansions of the
   instances (eta is allowed if the meta was applied to arguments)

   This used to fail before revision 9389 in trunk
*)

Lemma l5 :
   forall f : (forall P, P true), (forall P, f P = f P) ->
   forall Q, f (fun x => Q x) = f (fun x => Q x).
Proof.
intros.
apply H.
Qed.

(* Feature deactivated in commit 14189 (see commit log)
(* Test instantiation of evars by unification *)

Goal (forall x, 0 + x = 0 -> True) -> True.
intros; eapply H.
rewrite <- plus_n_Sm. (* should refine ?x with S ?x' *)
Abort.
*)

(* Check handling of identity equation between evars *)
(* The example failed to pass until revision 10623 *)

Lemma l6 :
  (forall y, (forall x, (forall z, y = 0 -> y + z = 0) -> y + x = 0) -> True)
  -> True.
intros.
eapply H.
intros.
apply H0. (* Check that equation ?n[H] = ?n[H] is correctly considered true *)
reflexivity.
Qed.

(* Check treatment of metas erased by K-redexes at the time of turning
   them to evas *)

Inductive nonemptyT (t : Type) : Prop := nonemptyT_intro : t -> nonemptyT t.
Goal True.
try case nonemptyT_intro. (* check that it fails w/o anomaly *)
Abort.

(* Test handling of return type and when it is decided to make the
   predicate dependent or not - see "bug" BZ#1851 *)

Goal forall X (a:X) (f':nat -> X), (exists f : nat -> X, True).
intros.
exists (fun n => match n with O => a | S n' => f' n' end).
constructor.
Qed.

(* Check use of types in unification (see Andrej Bauer's mail on
   coq-club, June 1 2009; it did not work in 8.2, probably started to
   work after Sozeau improved support for the use of types in unification) *)

Goal (forall (A B : Set) (f : A -> B), (fun x => f x) = f) ->
forall (A B C : Set) (g : (A -> B) -> C) (f : A -> B), g (fun x => f x) = g f.
Proof.
  intros.
  rewrite H with (f:=f0).
Abort.

(* Three tests provided by Dan Grayson as part of a custom patch he
   made for a more powerful "destruct" for handling Voevodsky's
   Univalent Foundations. The test checks if second-order matching in
   tactic unification is able to guess by itself on which dependent
   terms to abstract so that the elimination predicate is well-typed *)

Definition test1 (X : Type) (x : X) (fxe : forall x1 : X, identity x1 x1) :
  identity (fxe x) (fxe x).
Proof. destruct (fxe x). apply identity_refl. Defined.

(* a harder example *)

Definition UU := Type .
Inductive paths {T:Type}(t:T): T -> UU := idpath: paths t t.
Inductive foo (X0:UU) (x0:X0) : forall (X:UU)(x:X), UU := newfoo : foo x0 x0.
Definition idonfoo {X0:UU} {x0:X0} {X1:UU} {x1:X1} : foo x0 x1 -> foo x0 x1.
Proof. intros t. exact t. Defined.

Lemma test2 (T:UU) (t:T) (k : foo t t) : paths k (idonfoo k).
Proof.
  destruct k.
  apply idpath.
Defined.

(* an example with two constructors *)

Inductive foo' (X0:UU) (x0:X0) : forall (X:UU)(x:X), UU :=
| newfoo1 : foo' x0 x0
| newfoo2 : foo' x0 x0 .
Definition idonfoo' {X0:UU} {x0:X0} {X1:UU} {x1:X1} :
  foo' x0 x1 -> foo' x0 x1.
Proof. intros t. exact t. Defined.
Lemma test3 (T:UU) (t:T) (k : foo' t t) : paths k (idonfoo' k).
Proof.
  destruct k.
  apply idpath.
  apply idpath.
Defined.

(* An example where it is necessary to evar-normalize the instance of
   an evar to evaluate if it is a pattern *)

Check
  let a := ?[P] in
  fun (H : forall y (P : nat -> Prop), y = 0 -> P y)
      x (p:x=0) =>
    H ?[y] a p : x = 0.
(* We have to solve "?P ?y[x] == x = 0" knowing from
   "p : (x=0) == (?y[x] = 0)" that "?y := x" *)

(* An example involving SProp *)

Check fun (A:SProp) (f g:A->A) (P:A->Type) a (x : P (f a)) => x : P (g _).

quality98%

¤ Dauer der Verarbeitung: 0.284 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.