8000 Sealed goal for mode should be resumed if progress · Issue #17 · FissoreD/coq-elpi · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Sealed goal for mode should be resumed if progress #17

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Open
FissoreD opened this issue Jun 21, 2024 · 2 comments
Open

Sealed goal for mode should be resumed if progress #17

FissoreD opened this issue Jun 21, 2024 · 2 comments

Comments

@FissoreD
Copy link
Owner
FissoreD commented Jun 21, 2024 •
edited
Loading 
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
Copy link
Owner Author

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
Copy link
Owner Author
FissoreD commented Jun 26, 2024 •
edited
Loading

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.
}}.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@FissoreD
0