add corresponding documentation in book

add solution0

document solution0 and remove unecessary test cases

simplify according to review

Author: firefighterduck

book/src/recursive/coinduction.md

@@ -1,3 +1,73 @@
 # Coinduction
 
-TBD
+This sub-chapter is meant to describe the current handling of coinductive goals in the recursive solver rather than providing an extensive overview over the theoretical backgrounds and ideas.
+It follows the description in [this GitHub comment](https://github.com/rust-lang/chalk/issues/399#issuecomment-643420016) and the Zulip topic linked there.
+
+## General Idea
+The general idea for the handling of coinductive cycles in the recursive solver is to start by assuming the goal is provable and then try to find evidence that it is not.
+This search for a disproof is done by the standard recursive solving process described in the sub-chapters before.
+
+Albeit this approach would allow for the handling of mixed inductive/co-inductive cycles, these are actually handled as errors to prevent propagation of the assumed provability outside of the coinductive cycle.
+This propagation of the assumed solution might also happen in pure coinductive cycles and can potentially lead to invalid results.
+
+## Prevention of Invalid Results
+The problem of invalid results propagated outside of the coinductive cycle is also described in the [Coinduction chapter](../engine/logic/coinduction.md) for the SLG solver alongside the rather complex handling used with it.
+
+### The Problem
+The problem arises if a solution that is purely based on the positive starting value for the coinductive cycle is cached and as such propagated to other goals that are possibly reliant on this. An example may look like this (cf. the test case `coinduction::coinductive_unsound`):
+
+```notrust
+C :- C1.
+C :- C2
+C1 :- C2, C3.
+C2 :- C1.
+```
+
+Here `C` may be proved by either showing `C1` or `C2`.
+Assuming the solver starts evaluating the branch with `C1` first, it then recursively tries to prove `C2` and `C3`.
+For proving `C2` it needs to show `C1` again, the coinductive cycle becomes evident.
+Therefore, `C1` is assumed to be provable and the solver proves `C2` with this information.
+Assuming, the solve does not handle this case specifically, the solution for `C2` is cached. 
+Now it tries solving `C3` but fails due to the lack of information about it.
+As such, `C1` can also not be proven for this program.
+The recursive solver will now attempt to prove the initial goal `C` by solving `C2`.
+Unfortunately, it finds the invalidly cached solution and returns it as proof for `C`.
+
+By visualizing this path of computation, it becomes evident, where the problem lies:
+* Start proving `C` with `C1`:
+    * For `C1` prove `C2` and `C3`:
+        * For `C2` prove `C1`:
+            * This is a coinductive cycle. Assume that `C1` holds.
+        * Thus `C2` also holds. Store this result about `C2` in the cache.
+        * There is no way to prove `C3`. Lift this failure up.
+    * Due to the failure of `C3` there is also no solution for `C1`.
+* Try proving `C` with `C2`:
+    * Find the cached result that `C2` has a solution and return it as the solution for `C`.
+* Stop with the invalid result for `C`.
+
+### The Solution
+The above example should make it evident that the caching of found solutions in coinductive cycles can lead to invalid results and should therefore be prevented.
+This can be achieved by delaying the caching of all results inside the coinductive cycle until it is clear whether the start of the cycle (i.e. `C1` in the example above) is provable.
+If the start of the cycle can be proven by the results of the cycle and related subgoals then the assumption about it was correct and thus all results for goals inside the cycle are also valid.
+If, however, the start of the cycle can not be proved, i.e. the initial assumption was false, then a subset of the found solutions for the coinductive cycle may be invalid (i.e. the solution for `C2` in the example).
+
+To remove such invalid results, the cycle is restarted with a negative result for the cycle start.
+With this approach, it is possible to remove all invalid result that would otherwise depend on the disproved cycle assumption.
+To allow for the cycle to be restarted correctly, all nodes in the search graph after the cycle start are deleted.
+
+With this procedure, the example is handled as follows:
+* Start proving `C` with `C1`:
+    * For `C1` prove `C2` and `C3`:
+        * For `C2` prove `C1`:
+            * This is a coinductive cycle. Assume that `C1` holds.
+        * Thus `C2` also holds. Delay the caching of the result about `C2`.
+        * There is no way to prove `C3`. Cache this result and lift the failure up.
+    * Due to the failure of `C3` there is also no solution for `C1`. Set `C1` to a negative result and restart the cycle.
+        * For `C2` prove `C1`:
+            * `C1` has now a negative result.
+        * Thus, `C2` also has a negative result which is not yet cached.
+        * The result for `C3` is already cached.
+    * Nothing changed regarding `C1` (this would indicate a negative cycle which is currently  not allowed) and the negative result for `C1` and `C2` are cached. Lift negative result for `C1`.
+* Start proving `C` with `C2`:
+    * Find negative cached result for `C2`. Lift the result back up.
+* Neither `C1` nor `C2` have a positive result. Stop with the valid disproof of `C`.

chalk-recursive/src/combine.rs

@@ -2,33 +2,7 @@ use chalk_solve::Solution;
 use tracing::debug;
 
 use chalk_ir::interner::Interner;
-use chalk_ir::{ClausePriority, DomainGoal, Fallible, GenericArg, Goal, GoalData};
-
-pub(crate) fn with_priorities_for_goal<I: Interner>(
-    interner: &I,
-    goal: &Goal<I>,
-    a: Fallible<Solution<I>>,
-    prio_a: ClausePriority,
-    b: Fallible<Solution<I>>,
-    prio_b: ClausePriority,
-) -> (Fallible<Solution<I>>, ClausePriority) {
-    let domain_goal = match goal.data(interner) {
-        GoalData::DomainGoal(domain_goal) => domain_goal,
-        _ => {
-            // non-domain goals currently have no priorities, so we always take the new solution here
-            return (b, prio_b);
-        }
-    };
-    match (a, b) {
-        (Ok(a), Ok(b)) => {
-            let (solution, prio) = with_priorities(interner, domain_goal, a, prio_a, b, prio_b);
-            (Ok(solution), prio)
-        }
-        (Ok(solution), Err(_)) => (Ok(solution), prio_a),
-        (Err(_), Ok(solution)) => (Ok(solution), prio_b),
-        (Err(_), Err(e)) => (Err(e), prio_b),
-    }
-}
+use chalk_ir::{ClausePriority, DomainGoal, GenericArg};
 
 pub(super) fn with_priorities<I: Interner>(
     interner: &I,

chalk-recursive/src/recursive.rs

@@ -2,10 +2,10 @@ use crate::search_graph::DepthFirstNumber;
 use crate::search_graph::SearchGraph;
 use crate::solve::{SolveDatabase, SolveIteration};
 use crate::stack::{Stack, StackDepth};
-use crate::{combine, Minimums, UCanonicalGoal};
-use chalk_ir::interner::Interner;
+use crate::{Minimums, UCanonicalGoal};
 use chalk_ir::Fallible;
-use chalk_ir::{Canonical, ConstrainedSubst, Constraints, Goal, InEnvironment, UCanonical};
+use chalk_ir::{interner::Interner, NoSolution};
+use chalk_ir::{Canonical, ConstrainedSubst, Goal, InEnvironment, UCanonical};
 use chalk_solve::{coinductive_goal::IsCoinductive, RustIrDatabase, Solution};
 use rustc_hash::FxHashMap;
 use std::fmt;
@@ -163,18 +163,6 @@ impl<'me, I: Interner> Solver<'me, I> {
                 return *minimums;
             }
 
-            let old_answer = &self.context.search_graph[dfn].solution;
-            let old_prio = self.context.search_graph[dfn].solution_priority;
-
-            let (current_answer, current_prio) = combine::with_priorities_for_goal(
-                self.program.interner(),
-                &canonical_goal.canonical.value.goal,
-                old_answer.clone(),
-                old_prio,
-                current_answer,
-                current_prio,
-            );
-
             // Some of our subgoals depended on us. We need to re-run
             // with the current answer.
             if self.context.search_graph[dfn].solution == current_answer {
@@ -223,37 +211,15 @@ impl<'me, I: Interner> SolveDatabase<I> for Solver<'me, I> {
         if let Some(dfn) = self.context.search_graph.lookup(&goal) {
             // Check if this table is still on the stack.
             if let Some(depth) = self.context.search_graph[dfn].stack_depth {
-                // Is this a coinductive goal? If so, that is success,
-                // so we can return and set the minimum to its DFN.
-                // Note that this return is not tabled. And so are
-                // all other solutions in the cycle until the cycle
-                // start is finished. This avoids prematurely cached
-                // false positives.
-                if self.context.stack.coinductive_cycle_from(depth) {
-                    let value = ConstrainedSubst {
-                        subst: goal.trivial_substitution(self.program.interner()),
-                        constraints: Constraints::empty(self.program.interner()),
-                    };
-                    let trivial_solution = Ok(Solution::Unique(Canonical {
-                        value,
-                        binders: goal.canonical.binders,
-                    }));
-
-                    debug!("applying coinductive semantics");
-
-                    // Set minimum to first occurrence of cyclic goal to prevent premature caching of possibly false solutions
-                    minimums.update_from(self.context.search_graph[dfn].links);
-
-                    // Store trivial solution to start coinductive reasoning from this node
-                    self.context.search_graph[dfn].solution = trivial_solution.clone();
-                    self.context.search_graph[dfn].solution_priority =
-                        chalk_ir::ClausePriority::Low;
-                    self.context.search_graph[dfn].coinductive_start = true;
-
-                    return trivial_solution;
-                }
-
                 self.context.stack[depth].flag_cycle();
+                // Mixed cycles are not allowed.
+                if self
+                    .context
+                    .stack
+                    .mixed_inductive_coinductive_cycle_from(depth)
+                {
+                    return Err(NoSolution);
+                }
             }
 
             minimums.update_from(self.context.search_graph[dfn].links);
@@ -268,10 +234,15 @@ impl<'me, I: Interner> SolveDatabase<I> for Solver<'me, I> {
             previous_solution
         } else {
             // Otherwise, push the goal onto the stack and create a table.
-            // The initial result for this table is error.
+            // The initial result for this table depends on whether the goal is coinductive.
             let coinductive_goal = goal.is_coinductive(self.program);
             let depth = self.context.stack.push(coinductive_goal);
-            let dfn = self.context.search_graph.insert(&goal, depth);
+            let dfn = self.context.search_graph.insert(
+                &goal,
+                depth,
+                coinductive_goal,
+                self.program.interner(),
+            );
             let subgoal_minimums = self.solve_new_subgoal(goal, depth, dfn);
             self.context.search_graph[dfn].links = subgoal_minimums;
             self.context.search_graph[dfn].stack_depth = None;
@@ -288,11 +259,6 @@ impl<'me, I: Interner> SolveDatabase<I> for Solver<'me, I> {
             // worst of the repeated work that we do during tabling.
             if subgoal_minimums.positive >= dfn {
                 if self.context.caching_enabled {
-                    // Remove possible false positives from coinductive cycle
-                    if self.context.search_graph[dfn].coinductive_start && result.is_err() {
-                        self.context.search_graph.remove_false_positives_after(dfn);
-                    }
-
                     self.context
                         .search_graph
                         .move_to_cache(dfn, &mut self.context.cache);

chalk-recursive/src/search_graph.rs

@@ -5,7 +5,10 @@ use std::usize;
 
 use super::stack::StackDepth;
 use crate::{Minimums, UCanonicalGoal};
-use chalk_ir::{interner::Interner, ClausePriority, Fallible, NoSolution};
+use chalk_ir::{
+    interner::Interner, Canonical, ClausePriority, ConstrainedSubst, Constraints, Fallible,
+    NoSolution,
+};
 use chalk_solve::Solution;
 use rustc_hash::FxHashMap;
 use tracing::{debug, instrument};
@@ -37,11 +40,6 @@ pub(super) struct Node<I: Interner> {
     /// from the stack, it contains the DFN of the minimal ancestor
     /// that the table reached (or MAX if no cycle was encountered).
     pub(crate) links: Minimums,
-
-    /// If this is true, the node is the start of coinductive cycle.
-    /// Thus, some cleanup has to be done before its result can be
-    /// cached to rule out false positives.
-    pub(crate) coinductive_start: bool,
 }
 
 impl<I: Interner> SearchGraph<I> {
@@ -61,22 +59,35 @@ impl<I: Interner> SearchGraph<I> {
     ///
     /// - stack depth as given
     /// - links set to its own DFN
-    /// - solution is initially `NoSolution`
+    /// - solution is initially an identity substitution for coinductive goals
+    ///   or `NoSolution` for other goals
     pub(crate) fn insert(
         &mut self,
         goal: &UCanonicalGoal<I>,
         stack_depth: StackDepth,
+        coinductive: bool,
+        interner: &I,
     ) -> DepthFirstNumber {
         let dfn = DepthFirstNumber {
             index: self.nodes.len(),
         };
+        let solution = if coinductive {
+            Ok(Solution::Unique(Canonical {
+                value: ConstrainedSubst {
+                    subst: goal.trivial_substitution(interner),
+                    constraints: Constraints::empty(interner),
+                },
+                binders: goal.canonical.binders.clone(),
+            }))
+        } else {
+            Err(NoSolution)
+        };
         let node = Node {
             goal: goal.clone(),
-            solution: Err(NoSolution),
+            solution,
             solution_priority: ClausePriority::High,
             stack_depth: Some(stack_depth),
             links: Minimums { positive: dfn },
-            coinductive_start: false,
         };
         self.nodes.push(node);
         let previous_index = self.indices.insert(goal.clone(), dfn);
@@ -107,32 +118,6 @@ impl<I: Interner> SearchGraph<I> {
             cache.insert(node.goal, node.solution);
         }
     }
-
-    /// Removes all nodes that are part of a coinductive cycle and
-    /// have a solution as they might be false positives due to
-    /// coinductive reasoning.
-    #[instrument(level = "debug", skip(self))]
-    pub(crate) fn remove_false_positives_after(&mut self, dfn: DepthFirstNumber) {
-        let mut false_positive_indices = vec![];
-
-        // Find all possible false positives in the graph below the
-        // start of the coinductive cycle
-        for (index, node) in self.nodes[dfn.index + 1..].iter().enumerate() {
-            if node.solution.is_ok() {
-                false_positive_indices.push(index + dfn.index + 1);
-            }
-        }
-
-        // Remove the potential false positives from the indices
-        self.indices
-            .retain(|_key, value| !false_positive_indices.contains(&value.index));
-
-        // Remove the potential false positives from the nodes
-        // in descending order to avoid unnecessary shifts
-        for false_positive_index in false_positive_indices.into_iter().rev() {
-            self.nodes.remove(false_positive_index);
-        }
-    }
 }
 
 impl<I: Interner> Index<DepthFirstNumber> for SearchGraph<I> {

chalk-recursive/src/stack.rs

@@ -67,12 +67,20 @@ impl Stack {
         self.entries.pop();
     }
 
-    /// True if all the goals from the top of the stack down to (and
-    /// including) the given depth are coinductive.
-    pub(crate) fn coinductive_cycle_from(&self, depth: StackDepth) -> bool {
-        self.entries[depth.depth..]
-            .iter()
-            .all(|entry| entry.coinductive_goal)
+    /// True if either all the goals from the top of the stack down to (and
+    /// including) the given depth are  coinductive or if all goals are inductive
+    /// (i.e. not coinductive).
+    pub(crate) fn mixed_inductive_coinductive_cycle_from(&self, depth: StackDepth) -> bool {
+        let (inductive, coinductive) =
+            self.entries[depth.depth..]
+                .iter()
+                .fold((false, false), |(ind, coind), entry| {
+                    (
+                        ind || !entry.coinductive_goal,
+                        coind || entry.coinductive_goal,
+                    )
+                });
+        inductive && coinductive
     }
 }