Templates in Rewriting Induction

This companion page for the paper Templates in Rewriting Induction shows the Cora proofs for the various recursors and the factorial systems in the paper, using bounded rewriting induction.

To download and install Cora, see the instructions for another submission. These instructions also explain how to invoke Cora's interactive equivalence prover, how to load a proof file and play around in the interactive system.

Recursors

You can download the input file containing all recursors here. This file also contains defined symbols "f" and "g", which are used to stand in for □₁ and □₂ in the proofs of the conditional inductive theorems. (The odd rules defining f and g are only there to ensure that Cora does not consider them as constructor symbols.)

Lemma 4.1

The unconditional equivalences are listed below:

• proof input for taildown f x y z ≈ recup f x y z (start cora recursors.lcstrs -e while you are in the directory that contains this file, then type taildownrecup.proof on the first line; this will execute the proof process; or just see Cora's proof output for taildown f x y z ≈ recup f x y z
• proof input for tailup f x y z ≈ recdown f x y z and Cora's proof output for tailup f x y z ≈ recdown f x y z

Lemma 4.8

And here are the conditional equivalences. These use the extra symbols f and g and they are not complete proofs, since they leave the axioms open as equations in the system. If those axioms could also be proved (with other terms taking the place of f and g) we would clearly have a complete proof.

• conditional proof input for tailup F x y z ≈ taildown G x y z and Cora's proof output for tailup F x y z ≈ taildown G x y z
• conditional proof input for tailup F x y z ≈ recup G x y z and Cora's proof output for tailup F x y z ≈ recup G x y z
• conditional proof input for taildown F x y z ≈ recdown G x y z and Cora's proof output for taildown F x y z ≈ recdown G x y z
• conditional proof input for recup F x y z ≈ recdown G x y z and Cora's proof output for recup F x y z ≈ recdown G x y z

Factorial equivalences

Now we see the proofs of the equivalences between the various forms of factorial

Example 4.2

factTU x ≈ factRD x | x ≥ 1: lcstrs input file with the rules for factTU and factRD (and corresponding recursors)

• proof input for factTU x ≈ factRD x using one-sided matching on the left and
  Cora's proof output for factTU x ≈ factRD x using one-sided matching on the left
• proof input for factTU x ≈ factRD x using one-sided matching on the right and
  Cora's proof output for factTU x ≈ factRD x using one-sided matching on the right

Example 4.3

• proof input for factTD x ≈ factRU x using one-sided matching on the left and
  Cora's proof output for factTD x ≈ factRU x using one-sided matching on the left
• proof input for factTD x ≈ factRU x using one-sided matching on the right and
  Cora's proof output for factTD x ≈ factRU x using one-sided matching on the right

Example 4.4

factTU x ≈ factRD x | x ≥ 1: lcstrs input file with the rules for factTU and factRD (and corresponding recursors)

• proof input for factTU x ≈ factRD x using two-sided matching and
  Cora's proof output for factTU x ≈ factRD x using two-sided matching

Example 4.5

• proof input for factTD x ≈ factRU x using two-sided matching and
  Cora's proof output for factTD x ≈ factRU x using two-sided matching
• proof input for factTD x ≈ factRU x using two-sided matching and
  Cora's proof output for factTD x ≈ factRU x using two-sided matching

Remaining factorial equivalences (not discussed in the paper)

• factTD x ≈ factRD x: lcstrs input file with the rules for factTD and factRD (and corresponding recursors)
  • proof input for factTD x ≈ factRD x using one-sided matching on the left and
    Cora's proof output for factTU x ≈ factRD x using one-sided matching on the left
• factTU x ≈ factTD x: lcstrs input file with the rules for factTU and factTD (and corresponding recursors)
  • proof input for factTU x ≈ factTD x using two-sided and
    Cora's proof output for factTU x ≈ factRD x using two-sided matching
• factTU x ≈ factRU x | x ≥ 1: lcstrs input file with the rules for factTU and factRU (and corresponding recursors)
  • proof input for factTU x ≈ factRU x using one-sided matching on the right and
    Cora's proof output for factTU x ≈ factRU x using one-sided matching on the right
  • proof input for factTU x ≈ factRU x using two-sided matching and
    Cora's proof output for factTU x ≈ factRU x using two-sided matching
• factRU x ≈ factRD x | x ≥ 1: lcstrs input file with the rules for factRU and factRD (and corresponding recursors)
  • proof input for factRU x ≈ factRD x using two-sided matching and
    Cora's proof output for factRU x ≈ factRD x using two-sided matching

Composite equivalence

Finally, let us consider the equivalence of Section 4.4:

• here's the input file for the funfactTU and funfactTD systems
• and here are the proof input for funfactTU h x ≈ funfactTD h x using two-sided matching, and Cora's proof output for funfactTU h x ≈ funfactTD h x; note that the proof starts with the two template-recursor equivalences and then the recursor equivalence which follows the shape of the conditional inductive theorem we saw before

In this case, Cora actually fails to find the termination proof automatically. This is because of the use of static dependency pairs for the termination check in the current version of Cora, where for instance taildown(helperG(h), x1, y, h(x) * a) is not considered a valid left-hand side because the higher-order variable h occurs applied.

Nevertheless, we can see that the ordering requirements can be satisfied, since they are captured by the following terminating term rewriting system (presented in Cora notation)::

• helperF(h) → helperG(h)
• helperG(h, x, y) → h(x)
• tailup(HELPERVAR, x, y, a) → taildown(HELPERVAR, x1, y, HELPERVAR(x,0) * a) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1
• taildown(HELPERVAR, x1, y, u * v) → v * u | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 ∧ ¬(x1 ≤ y)
• taildown(HELPERVAR, x1, y, u * a) → taildown(HELPERVAR, x1, y1, u * (a * HELPERVAR(y,0))) | x ≤ y ∧ x1 = x + 1 ∧ y1 = y - 1 ∧ x1 ≤ y ∧ y2 = y1 - 1
• funfactTD(h, x) → taildown(helperG(h), 1, x, 1)
• funfactTU(h, x) → tailup(helperF(h), 1, x, 1)

In the future, we hope to adapt Cora to find such termination abstractions automatically.