| products/sources/formale sprachen/Coq/plugins/omega/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: autoclean.v Sprache: CoqOriginal von: Coq© |
|
||||||
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *) (* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (* * (see LICENSE file for the text of the license) *) (************************************************************************) Class A (A : Type). Instance an: A nat := {}. Class B (A : Type) (a : A). Instance bn0: B nat 0 := {}. Instance bn1: B nat 1 := {}. Goal A nat. Proof. typeclasses eauto. Qed. Goal B nat 2. Proof. Fail typeclasses eauto. Abort. Goal exists T : Type, A T. Proof. eexists. typeclasses eauto. Defined. Hint Extern 0 (_ /\ _) => constructor : typeclass_instances. Existing Class and. Goal exists (T : Type) (t : T), A T /\ B T t. Proof. eexists. eexists. typeclasses eauto. Defined. Instance ab: A bool := {}. (* Backtrack on A instance *) Goal exists (T : Type) (t : T), A T /\ B T t. Proof. eexists. eexists. typeclasses eauto. Defined. Class C {T} `(a : A T) (t : T). Require Import Classes.Init. Hint Extern 0 { x : ?A & _ } => unshelve class_apply @existT : typeclass_instances. Existing Class sigT. Set Typeclasses Debug. Instance can: C an 0 := {}. (* Backtrack on instance implementation *) Goal exists (T : Type) (t : T), { x : A T & C x t }. Proof. eexists. eexists. typeclasses eauto. Defined. Class D T `(a: A T). Instance: D _ an := {}. Goal exists (T : Type), { x : A T & D T x }. Proof. eexists. typeclasses eauto. Defined. (* Example from Nicolas Magaud on coq-club - Jul 2000 *) Definition Nat : Set := nat. Parameter S' : Nat -> Nat. Parameter plus' : Nat -> Nat -> Nat. Lemma simpl_plus_l_rr1 : (forall n0 : Nat, (forall m p : Nat, plus' n0 m = plus' n0 p -> m = p) -> forall m p : Nat, S' (plus' n0 m) = S' (plus' n0 p) -> m = p) -> forall n : Nat, (forall m p : Nat, plus' n m = plus' n p -> m = p) -> forall m p : Nat, S' (plus' n m) = S' (plus' n p) -> m = p. intros. apply H0. apply f_equal_nat. Time info_eauto. Undo. Set Typeclasses Debug. Set Typeclasses Iterative Deepening. Time typeclasses eauto 6 with nocore. Show Proof. Undo. Time eauto. (* does EApply H *) Qed. (* Example from Nicolas Tabareau on coq-club - Feb 2016. Full backtracking on dependent subgoals. *) Require Import Coq.Classes.Init. Module NTabareau. Set Typeclasses Dependency Order. Unset Typeclasses Iterative Deepening. Notation "x .1" := (projT1 x) (at level 3). Notation "x .2" := (projT2 x) (at level 3). Parameter myType: Type. Class Foo (a:myType) := {}. Class Bar (a:myType) := {}. Class Qux (a:myType) := {}. Parameter fooTobar : forall a (H : Foo a), {b: myType & Bar b}. Parameter barToqux : forall a (H : Bar a), {b: myType & Qux b}. Hint Extern 5 (Bar ?D.1) => destruct D; simpl : typeclass_instances. Hint Extern 5 (Qux ?D.1) => destruct D; simpl : typeclass_instances. Hint Extern 1 myType => unshelve refine (fooTobar _ _).1 : typeclass_instances. Hint Extern 1 myType => unshelve refine (barToqux _ _).1 : typeclass_instances. Hint Extern 0 { x : _ & _ } => simple refine (existT _ _ _) : typeclass_instances. Unset Typeclasses Debug. Definition trivial a (H : Foo a) : {b : myType & Qux b}. Proof. Time typeclasses eauto 10 with typeclass_instances. Undo. Set Typeclasses Iterative Deepening. Time typeclasses eauto with typeclass_instances. Defined. End NTabareau. Module NTabareauClasses. Set Typeclasses Dependency Order. Unset Typeclasses Iterative Deepening. Notation "x .1" := (projT1 x) (at level 3). Notation "x .2" := (projT2 x) (at level 3). Parameter myType: Type. Existing Class myType. Class Foo (a:myType) := {}. Class Bar (a:myType) := {}. Class Qux (a:myType) := {}. Parameter fooTobar : forall a (H : Foo a), {b: myType & Bar b}. Parameter barToqux : forall a (H : Bar a), {b: myType & Qux b}. Hint Extern 5 (Bar ?D.1) => destruct D; simpl : typeclass_instances. Hint Extern 5 (Qux ?D.1) => destruct D; simpl : typeclass_instances. Hint Extern 1 myType => unshelve notypeclasses refine (fooTobar _ _).1 : typeclass_instances. Hint Extern 1 myType => unshelve notypeclasses refine (barToqux _ _).1 : typeclass_instances. Hint Extern 0 { x : _ & _ } => unshelve notypeclasses refine (existT _ _ _) : typeclass_instances. Unset Typeclasses Debug. Definition trivial a (H : Foo a) : {b : myType & Qux b}. Proof. Time typeclasses eauto 10 with typeclass_instances. Undo. Set Typeclasses Iterative Deepening. (* Much faster in iteratove deepening mode *) Time typeclasses eauto with typeclass_instances. Defined. End NTabareauClasses. Require Import List. Parameter in_list : list (nat * nat) -> nat -> Prop. Definition not_in_list (l : list (nat * nat)) (n : nat) : Prop := ~ in_list l n. (* Hints Unfold not_in_list. *) Axiom lem1 : forall (l1 l2 : list (nat * nat)) (n : nat), not_in_list (l1 ++ l2) n -> not_in_list l1 n. Axiom lem2 : forall (l1 l2 : list (nat * nat)) (n : nat), not_in_list (l1 ++ l2) n -> not_in_list l2 n. Axiom lem3 : forall (l : list (nat * nat)) (n p q : nat), not_in_list ((p, q) :: l) n -> not_in_list l n. Axiom lem4 : forall (l1 l2 : list (nat * nat)) (n : nat), not_in_list l1 n -> not_in_list l2 n -> not_in_list (l1 ++ l2) n. Hint Resolve lem1 lem2 lem3 lem4: essai. Goal forall (l : list (nat * nat)) (n p q : nat), not_in_list ((p, q) :: l) n -> not_in_list l n. intros. eauto with essai. Qed. ¤ Dauer der Verarbeitung: 0.19 Sekunden (vorverarbeitet) ¤ |
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.Bot Zugriff |
