search

FissoreD / coq-elpi

Coq plugin embedding elpi
GNU Lesser General Public License v2.1
0 stars 0 forks source link

Sealed goal for mode should be resumed if progress #17

Open FissoreD opened 3 weeks ago

FissoreD commented 3 weeks ago 
From elpi Require Import elpi.
From elpi Require Import tc.

  TC.Pending_mode !.
  Class A (i: Type).
  Global Hint Mode A ! : typeclass_instances.

  Class B (i :Type).

  Instance a: A nat := {}.
  Instance b: B nat := {}.

  Goal exists X, A X /\ B X.
    eexists; split.
    all: elpi TC.Solver.
    (* Here there should be no goal left *)
  Qed.

What happens: we receive the list of goals: A X and B X. Expected : Solving A X fails due to modes. B X succeeds with b setting X to nat. A nat is resumed for resolution Actual behaviour: A X fails due to modes. B X succeeds with b setting X to nat. A nat is not resumed but returned as new goal.

FissoreD commented 2 weeks ago

Another example:

From elpi Require Import elpi.
From elpi Require Import tc.

  TC.Pending_mode ! ! -.
  Class A (i: Type) (i : Type) (i: Type).
  Global Hint Mode A ! ! - : typeclass_instances.

  Class B (i :Type).
  Class C (c :Type).
  Class D (c :Type).
  Global Hint Mode D ! : typeclass_instances.

  Instance a: A nat nat nat := {}.
  Instance b: B nat := {}.
  Definition aaa := True.
  Instance c: C nat := {}.
  Instance d: D nat := {}.

  Goal exists X Y Z, A X Y Z /\ B X /\ C Y /\ D Z.
    do 3 (eexists).
    split; [|split; [|split]].
    all: typeclasses eauto.
    all: elpi TC.Solver.
    (* Here there should be no goal left *)
  Qed.
FissoreD commented 2 weeks ago

A raw solution:

Elpi Accumulate TC.Solver lp:{{
  pred is-seal-mode i:sealed-goal, o:sealed-goal.
  is-seal-mode (seal-mode S) S :- !.
  is-seal-mode (seal G) (seal G) :- !.
  is-seal-mode (nabla B) (nabla C) :- pi x\ is-seal-mode (B x) (C x).

  pred partition-clean-s-mode i:list A, o:list B, o:list A.
  partition-clean-s-mode [] [] [] :- !.
  partition-clean-s-mode [H|L] [A|M] N :- is-seal-mode H A, !, partition-clean-s-mode L M N.
  partition-clean-s-mode [H|L] M [H|N] :- partition-clean-s-mode L M N.

  type seal-mode sealed-goal -> sealed-goal.

  :after "0"
  refine-proof tc.mode_fail G [seal-mode (seal G)] :- !.
  :after "0" 
  msolve L N :-
    std.length L Len,
    time-it oTC-time-msolve (coq.ltac.all (coq.ltac.open solve-aux) L N') "msolve",
    partition-clean-s-mode N' SealMode Seal,
    if2 (SealMode = []) (N = N') 
        (std.length SealMode Len) (N = SealMode)
        (msolve SealMode N'', std.append Seal N'' N).
  :after "1"
  msolve L _ :-
    coq.ltac.fail _ "[TC] fail to solve" L.
}}.