Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: bteauto.v Sprache: Coq

Original von: Coq^©

Require Import Program.Tactics.
Module Backtracking.
  Class A := { foo : nat }.

  Instance A_1 : A | 2 := { foo := 42 }.
  Instance A_0 : A | 1 := { foo := 0 }.
  Lemma aeq (a : A) : foo = foo.
    reflexivity.
  Qed.

  Arguments foo A : clear implicits.
  Example find42 : exists n, n = 42.
  Proof.
    eexists.
    eapply eq_trans.
    evar (a : A). subst a.
    refine (@aeq ?a).
    Unshelve. all:cycle 1.
    typeclasses eauto.
    Fail reflexivity.
    Undo 2.
    (* Without multiple successes it fails *)
    Set Typeclasses Debug Verbosity 2.
    Fail all:((once (typeclasses eauto with typeclass_instances))
              + apply eq_refl).
    (* Does backtrack if other goals fail *)
    all:[> typeclasses eauto + reflexivity .. ].
    Undo 1.
    all:(typeclasses eauto + reflexivity). (* Note "+" is a focussing combinator *)
    Show Proof.
  Qed.

  Print find42.

  Hint Extern 0 (_ = _) => reflexivity : equality.

  Goal exists n, n = 42.
    eexists.
    eapply eq_trans.
    evar (a : A). subst a.
    refine (@aeq ?a).
    Unshelve. all:cycle 1.
    typeclasses eauto.
    Fail reflexivity.
    Undo 2.

    (* Does backtrack between individual goals *)
    Set Typeclasses Debug.
    all:(typeclasses eauto with typeclass_instances equality).
  Qed.

  Unset Typeclasses Debug.

  Module Leivant.
    Axiom A : Type.
    Existing Class A.
    Axioms a b c d e: A.
    Existing Instances a b c d e.

    Ltac get_value H := eval cbv delta [H] in H.

    Goal True.
      Fail refine (let H := _ : A in _); let v := get_value H in idtac v; fail.
    Admitted.

    Goal exists x:A, x=a.
      unshelve evar (t : A). all:cycle 1.
      refine (@ex_intro _ _ t _).
      all:cycle 1.
      all:(typeclasses eauto + reflexivity).
    Qed.
  End Leivant.
End Backtracking.

Hint Resolve 100 eq_sym eq_trans : core.
Hint Cut [(_)* eq_sym eq_sym] : core.
Hint Cut [_* eq_trans eq_trans] : core.
Hint Cut [_* eq_trans eq_sym eq_trans] : core.

Goal forall x y z : nat, x = y -> z = y -> x = z.
Proof.
  intros.
  typeclasses eauto with core.
Qed.

Module Hierarchies.
  Class A := mkA { data : nat }.
  Class B := mkB { aofb :> A }.

  Existing Instance mkB.

  Definition makeB (a : A) : B := _.
  Definition makeA (a : B) : A := _.

  Fail Timeout 1 Definition makeA' : A := _.

  Hint Cut [_* mkB aofb] : typeclass_instances.
  Fail Definition makeA' : A := _.
  Fail Definition makeB' : B := _.
End Hierarchies.

(** Hint modes *)

Class Equality (A : Type) := { eqp : A -> A -> Prop }.

Check (eqp 0%nat 0).

Instance nat_equality : Equality nat := { eqp := eq }.

Instance default_equality A : Equality A | 1000 :=
  { eqp := eq }.

Check (eqp 0%nat 0).

(* Defaulting *)
Check (fun x y => eqp x y).
(* No more defaulting, reduce "trigger-happiness" *)
Definition ambiguous x y := eqp x y.

Hint Mode Equality ! : typeclass_instances.
Fail Definition ambiguous' x y := eqp x y.
Definition nonambiguous (x y : nat) := eqp x y.

(** Typical looping instances with defaulting: *)
Definition flip {A B C} (f : A -> B -> C) := fun x y => f y x.

Class SomeProp {A : Type} (f : A -> A -> A) :=
  { prf : forall x y, f x y = f x y }.

Instance propflip (A : Type) (f : A -> A -> A) :
  SomeProp f -> SomeProp (flip f).
Proof.
  intros []. constructor. reflexivity.
Qed.

Fail Timeout 1 Check prf.

Hint Mode SomeProp + + : typeclass_instances.
Check prf.
Check (fun H : SomeProp plus => _ : SomeProp (flip plus)).

(** Iterative deepening / breadth-first search *)

Module IterativeDeepening.

  Class A.
  Class B.
  Class C.

  Instance: B -> A | 0 := {}.
  Instance: C -> A | 0 := {}.
  Instance: C -> B -> A | 0 := {}.
  Instance: A -> A | 0 := {}.

  Goal C -> A.
    intros.
    Fail Timeout 1 typeclasses eauto.
    Set Typeclasses Iterative Deepening.
    Fail typeclasses eauto 1.
    typeclasses eauto 2.
    Undo.
    Unset Typeclasses Iterative Deepening.
    Fail Timeout 1 typeclasses eauto.
    Set Typeclasses Iterative Deepening.
    Typeclasses eauto := debug 3.
    typeclasses eauto.
  Qed.

End IterativeDeepening.

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.