solve_ndisj taking a long time
The solve_ndisj
tactic takes a long time in certain situations. One such situation is captured by the included code.
From stdpp Require Import namespaces strings.
Section with_Σ.
Context (N : namespace).
Definition name_parentA := "Jesper".
Definition nameA := "Freya".
Definition name_parentB := "Robbert".
Definition nameB := "Jonas".
Lemma test : (((↑N ∖ ↑N.@name_parentB.@"children".@nameB.@"children"
∖ (↑N.@name_parentB.@"children" ∖ ↑N.@name_parentB.@"childreN".@nameB)):coPset) ⊆
((↑N ∖ ↑N.@name_parentA.@"children".@nameA.@"children".@"self".@"inv"):coPset)).
Proof.
time try solve_ndisj. (* This takes a long time *)
Admitted.
End with_Σ.
When run with Typeclasses eauto := debug
it produces ~25k lines of debug messages, which seem to be looping.
A snippet of the print outs can be seen here:
Debug: 1: looking for (Symmetric disjoint) without backtracking
Debug: 1.1: simple apply @Equivalence_Symmetric on (Symmetric disjoint), 1 subgoal(s)
Debug: 1.1-1 : (Equivalence disjoint)
Debug: 1.1-1: looking for (Equivalence disjoint) without backtracking
Debug: 1.1-1: no match for (Equivalence disjoint), 24 possibilities
Debug: 1.2: simple apply @PER_Symmetric on (Symmetric disjoint), 1 subgoal(s)
Debug: 1.2-1 : (RelationClasses.PER disjoint)
Debug: 1.2-1: looking for (RelationClasses.PER disjoint) without backtracking
Debug: 1.2-1.1: simple apply @Equivalence_PER on (RelationClasses.PER disjoint), 1 subgoal(s)
Debug: 1.2-1.1-1 : (Equivalence disjoint)
Debug: 1.2-1.1-1: looking for (Equivalence disjoint) without backtracking
Debug: 1.2-1.1-1: no match for (Equivalence disjoint), 24 possibilities
Debug: 1.3: simple eapply @disjoint_sym on (Symmetric disjoint), 1 subgoal(s)
Debug: 1.3-1 : (SemiSet positive coPset)
Debug: 1.3-1: looking for (SemiSet positive coPset) with backtracking
Debug: 1.3-1.1: exact set_semi_set on (SemiSet positive coPset), 0 subgoal(s)
Debug: 1: looking for (Symmetric disjoint) without backtracking
Debug: 1.1: simple apply @Equivalence_Symmetric on (Symmetric disjoint), 1 subgoal(s)
Debug: 1.1-1 : (Equivalence disjoint)
Debug: 1.1-1: looking for (Equivalence disjoint) without backtracking
Debug: 1.1-1: no match for (Equivalence disjoint), 24 possibilities
Debug: 1.2: simple apply @PER_Symmetric on (Symmetric disjoint), 1 subgoal(s)
Debug: 1.2-1 : (RelationClasses.PER disjoint)
Debug: 1.2-1: looking for (RelationClasses.PER disjoint) without backtracking
Debug: 1.2-1.1: simple apply @Equivalence_PER on (RelationClasses.PER disjoint), 1 subgoal(s)
Debug: 1.2-1.1-1 : (Equivalence disjoint)
Debug: 1.2-1.1-1: looking for (Equivalence disjoint) without backtracking
Debug: 1.2-1.1-1: no match for (Equivalence disjoint), 24 possibilities
Debug: 1.3: simple eapply @disjoint_sym on (Symmetric disjoint), 1 subgoal(s)
Debug: 1.3-1 : (SemiSet positive coPset)
Debug: 1.3-1: looking for (SemiSet positive coPset) with backtracking
Debug: 1.3-1.1: exact set_semi_set on (SemiSet positive coPset), 0 subgoal(s)