mattam82/coq-equations

A function definition package for Coq

Equations - a function definition plugin.

Copyright 2009-2022 Matthieu Sozeau [email protected] Copyright 2015-2018 Cyprien Mangin [email protected]

Distributed under the terms of the GNU Lesser General Public License Version 2.1 or later (see LICENSE for details).

Equations provides a notation for writing programs by dependent pattern-matching and (well-founded) recursion in Coq. It compiles everything down to eliminators for inductive types, equality and accessibility, providing a definitional extension to the Coq kernel. The plugin can be used with Coq's standard logic in Prop for a proof-irrelevant, erasable interpretation of pattern-matching, or with a polymorphic logic in Type or re-using the prelude of the HoTT/Coq library for a proof-relevant interpretation. In all cases, the resulting definitions are axiom-free.

Table of Contents

• Documentation
• Papers
• Gallery
• Installation
• HoTT Variant

Live demo

Try it now in your browser with JSCoq!

Documentation

• The reference manual provides an introduction and a summary of the commands and options. This introduction can also be followed interactively with Equations installed: equations_intro.v

• A gallery of examples provides more consequent developments using Equations.

Papers and presentations

• Equations Reloaded: High-Level Dependently-Typed Functional Programming and Proving in Coq. Matthieu Sozeau and Cyprien Mangin. In: Proc. ACM Program. Lang. 3, ICFP, Article 86 (August 2019), 29 pages. DOI, slides.

  This presents version 1.2 and above of the package. See Equations Reloaded for associated material, including a VM to run the examples.

• Equations for HoTT. Matthieu Sozeau, Talk given at the Homotopy Type Theory 2019 Conference in Pittsburgh, PA, August 2019.

  This explains the no-confusion principle and strong equivalences used by Equations and Jesper Cockx's version of dependent pattern-matching in Agda in terms of HoTT.

• Equations for Hereditary Substitution in Leivant's Predicative System F: A Case Study. Cyprien Mangin and Matthieu Sozeau. In: Proceedings Tenth International Workshop on Logical Frameworks and Meta Languages: Theory and Practice. Volume 185 of EPTCS. May 2015 - LFMTP'15.

  This is a case study on a proof of normalization for an hereditary substitution procedure on a variant of System F.

• Equations: A Dependent Pattern-Matching Compiler Matthieu Sozeau (2010) In: Kaufmann M., Paulson L.C. (eds) Interactive Theorem Proving. ITP 2010. Lecture Notes in Computer Science, vol 6172. Springer, Berlin, Heidelberg.

  This presents an earlier version of the package.

Installation

The latest version works with Coq 8.13 (branch 8.13), Coq 8.14 (branch 8.14), Coq 8.15 (branch 8.15), and the current Coq main branch (branch main).

See releases for sources and official releases.

Install with OPAM

This package is available on OPAM. Activate the Coq repository if you didn't do it yet:

opam repo add coq-released https://coq.inria.fr/opam/released

and run:

opam install coq-equations

To get the beta versions of Coq, activate the repository:

opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev

To get the development version of Equations, activate the repository:

opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev

Install from source

Alternatively, to compile Equations, simply run:

./configure.sh
make

in the toplevel directory, with coqc and ocamlc in your path.

Optionally, one can build the test-suite or examples:

make examples test-suite

Then add the paths to your .coqrc:

Add ML Path "/Users/mat/research/coq/equations/src".
Add Rec LoadPath "/Users/mat/research/coq/equations/theories" as Equations.

Or install it:

make install

As usual, you will need to run this command with the appropriate privileges if the version of Coq you are using is installed system-wide, rather than in your own directory. E.g. on Ubuntu, you would prefix the command with sudo and then enter your user account password when prompted.

HoTT Variant

The HoTT variant of Equations works with the coq-hott library for Coq 8.13 and up. When using opam, simply install first the coq-hott library and coq-equations will install its HoTT variant. From source, first install coq-hott and then use:

./configure.sh --enable-hott

This will compile the HoTT library variant in addition to the standard one. Then, after make install, one can import the plugin in Coq, using:

From Equations Require Import HoTT.All.

coq-equations's Issues

Unbound module Sigma?

I'm trying to build Coq-Equations myself with Coq 8.7, but I run into this build failure:

File "src/equations_common.mli", line 380, characters 18-28:
Error: Unbound module Sigma

Is there a dependency not specified in the README.md?

Use Subterm for noCycle?

After a short discussion with @mattam82 , it seems that it might be possible to build noCycle using well-foundedness of Subterm.

Unfold obligation not auto-solved, and not auto-proved equal to function

Here we have an unexpected second obligation related to the unfolded version, and an unexpected third obligation (remaining at the end, after a long wait for Coq to try hard to prove it) to prove that the unfolded version is equal to the original function.

Inductive TupleT : nat -> Type :=
nilT : TupleT 0
| consT {n} A : (A -> TupleT n) -> TupleT (S n).

Require Import Equations.

Ltac wf_subterm := intro;
  simp_exists;
  on_last_hyp depind; split; intros; simp_exists;
    on_last_hyp ltac:(fun H => red in H);
    [ exfalso | ];
    on_last_hyp depind;
    intuition.

Inductive Tuple : forall n, TupleT n -> Type :=
  nil : Tuple _ nilT
| cons {n A} (x : A) (F : A -> TupleT n) : Tuple _ (F x) -> Tuple _ (consT A F).

Inductive TupleMap : forall n, TupleT n -> TupleT n -> Type :=
  tmNil : TupleMap _ nilT nilT
| tmCons {n} {A B} (F : A -> TupleT n) (G : B -> TupleT n)
  : (forall x, sigT (TupleMap _ (F x) ∘ G)) -> TupleMap _ (consT A F) (consT B G).

Derive Signature for TupleMap.

Program Instance TupleMap_depelim n T U : DependentEliminationPackage (TupleMap n T U)
:= { elim_type := ∀ (P : forall n t t0, TupleMap n t t0 -> Type),
   P _ _ _ tmNil ->
  (∀ n A B (F : A -> TupleT n) (G : B -> TupleT n)
    (s : ∀ x, sigT (TupleMap _ (F x) ∘ G))
    (r : ∀ x, P _ _ _ (projT2 (s x))),
    P _ _ _ (tmCons F G s))
  -> ∀ (tm : TupleMap n T U), P _ _ _ tm }.
Next Obligation.
  revert n T U tm.
  fix IH 4.
  intros.
  Ltac destruct' x := destruct x.
  on_last_hyp destruct'; [ | apply X0 ]; auto.
Defined.

(* Doesn't know how to deal with the nested TupleMap 
   Derive Subterm for TupleMap. *)

Inductive TupleMap_direct_subterm
              : ∀ (n : nat) (H H0 : TupleT n) (n0 : nat) 
                (H1 H2 : TupleT n0),
                TupleMap n H H0 → TupleMap n0 H1 H2 → Prop :=
    TupleMap_direct_subterm_0_0 : ∀ (n : nat) (H H0 : TupleT n) 
                                  (n0 : nat) (H1 H2 : TupleT n0) 
                                  (n1 : nat) (H3 H4 : TupleT n1)
                                  (x : TupleMap n H H0)
                                  (y : TupleMap n0 H1 H2)
                                  (z : TupleMap n1 H3 H4),
                                  TupleMap_direct_subterm n H H0 n0 H1 H2 x y
                                  → TupleMap_direct_subterm n0 H1 H2 n1 H3 H4
                                      y z
                                    → TupleMap_direct_subterm n H H0 n1 H3 H4
                                        x z
|   TupleMap_direct_subterm_1_1 : ∀ n {A B} (F : A -> TupleT n) (G : B -> TupleT n)
  (H : forall x, sigT (TupleMap _ (F x) ∘ G)) (x : A),
  TupleMap_direct_subterm _ _ (G (projT1 (H _))) _ _ _ (projT2 (H x)) (tmCons _ _ H).

Definition TupleMap_subterm := 
λ x y : {index : {n : nat & sigT (λ _ : TupleT n, TupleT n)} &
     TupleMap (projT1 index) (projT1 (projT2 index)) (projT2 (projT2 index))},
TupleMap_direct_subterm (projT1 (projT1 x)) (projT1 (projT2 (projT1 x)))
  (projT2 (projT2 (projT1 x))) (projT1 (projT1 y))
  (projT1 (projT2 (projT1 y))) (projT2 (projT2 (projT1 y))) 
  (projT2 x) (projT2 y).

Program Instance WellFounded_TupleMap_subterm : WellFounded TupleMap_subterm.
Solve All Obligations using wf_subterm.

Equations(noind) myComp {n} {B C : TupleT n} (tm1 : TupleMap _ B C) {A : TupleT n} (tm2 : TupleMap _ A B)
: TupleMap _ A C :=
myComp n B C tm1 A tm2 by rec tm1 TupleMap_subterm :=
myComp ?(0) ?(nilT) ?(nilT) tmNil ?(nilT) tmNil := tmNil;
myComp ?(S _) ?(consT _ _) ?(consT _ _) (tmCons G H g) (consT _ _) (tmCons F ?(G) f)
:= tmCons _ _ (fun x => existT (fun y => TupleMap _ _ (_ y)) (projT1 (g (projT1 (f x)))) _).
Next Obligation.
  refine (myComp _ (existT _ _ _) (projT2 (g (projT1 (f x)))) _ _ (projT2 (f x))).
  apply (TupleMap_direct_subterm_1_1 _ _ _ g).
Defined.
Next Obligation.
  (* XXX: Should be solved automatically *)
  exact (myComp (projT2 (g (projT1 (f x)))) (projT2 (f x))).
Defined.
(* Obligation remaining *)

I have a hunch that this is due to a sigT containing a sigT only being partially unpacked (the outer sigT is unpacked, but not the inner) in the type of the first obligation.

Measure for a function of two arguments

I'm trying to define the interleave function as follows:

From Coq Require Import Arith List.
From Equations Require Import Equations.

Equations interleave {A} (l l' : list A) : list A :=
interleave l l' by rec (length l + length l') lt :=
interleave nil l' := l';
interleave (cons a l) l' := a :: interleave l' l.
Next Obligation.

But for some reason Equations unfolds the add and length functions, so I see the following obligation:

  (fix add (n m : nat) {struct n} : nat :=
     match n with
     | 0 => m
     | S p => S (add p m)
     end)
    ((fix length (l0 : list A1) : nat :=
        match l0 with
        | [] => 0
        | _ :: l'0 => S (length l'0)
        end) l')
    ((fix length (l0 : list A1) : nat :=
        match l0 with
        | [] => 0
        | _ :: l'0 => S (length l'0)
        end) l) <
  S
    ((fix add (n m : nat) {struct n} : nat :=
        match n with
        | 0 => m
        | S p => S (add p m)
        end)
       ((fix length (l0 : list A1) : nat :=
           match l0 with
           | [] => 0
           | _ :: l'0 => S (length l'0)
           end) l)
       ((fix length (l0 : list A1) : nat :=
           match l0 with
           | [] => 0
           | _ :: l'0 => S (length l'0)
           end) l'))

instead of

length l' + length l < length (a :: l) + length l'

How do I prevent this?

Have access to the body of a recursive function while defining it

Program Fixpoint and Equations here generate an obligation which is not provable. This example can be solved by refining the return type of f, but in general I wonder whether it could be possible to have access to the rewrite lemmas generated by Equations, while proving the obligations generated in the function. It should be sound to have access the rewrite lemmas for smaller recursive calls.

Require Equations.Equations.
      
Equations f (n: nat): nat :=
  f n := match n with
         | 0 => 0
         | S n' =>
           let H: f n' = 0 := _ in
           0
         end.

Next Obligation.
  (* Prove f n' = 0, given f: nat -> nat *)
Abort.

funind fails for subtraction using fins

Below I have copy-pasted the Ltac for funind from doc/intro.v, because sometimes this version of funind works for me when the default implementation of funind does not. However, in this particular case, neither version works.

Require Import Fin.

Require Import Equations.

Equations(nocomp) promote {n} m (i : fin (S n)) : fin (S (n + m)) :=
promote (S n) m (fs ?(S n) i) := fs (promote m i);
promote n m (fz ?(n)) := fz.

Lemma fog_promote_gof {j} k : j = fog (promote k (gof j)).
Proof with auto with arith. intros.
  funind (gof j) gofj.
  progress simp fog promote gof...
Qed.

Require Import Omega.

Equations minus' (n : nat) (m : fin (S n)) : fin (S n) :=
  minus' ?(S n) (fs (S n) m) := _ (promote 1 (minus' n m));
  minus' ?(n) (fz n) := gof n.
Next Obligation.
  red.
  replace (S n) with (n + 1) by abstract omega.
  assumption.
Defined.
Next Obligation.
  destruct n0; solve_equation minus'.
Defined.

Ltac funind c Hcall ::= 
  match c with
    appcontext C [ ?f ] => 
      let x := constr:(fun_ind_prf (f:=f)) in
        (let prf := eval simpl in x in
         let p := context C [ prf ] in
         let prf := fresh in
         let call := fresh in
           assert(prf:=p) ;
           (* Abstract the call *)
           set(call:=c) in *; generalize (refl_equal : call = c); clearbody call ; intro Hcall ;
           (* Now do dependent elimination and simplifications *)
           dependent induction prf ; simplify_IH_hyps)
           (* Use the simplifiers for the constant to get a nicer goal. *)
           (* try on_last_hyp ltac:(fun id => simpc f in id ; noconf id)) *)
        || fail 1 "Internal error in funind"
  end || fail "Maybe you didn't declare the functional induction principle for" c.

Ltac funelim c :=
  match c with
    appcontext C [ ?f ] => 
      let x := constr:(fun_elim (f:=f)) in
        (let prf := eval simpl in x in
          dependent pattern c ; apply prf)
  end.

Lemma minus'_eq (n : nat) (m : fin (S n)) : n - fog m = fog (minus' n m).
Proof.
  funind minus' H.

Need annotation for structurally-recursive argument

As mentioned in issue 8.

git grep Obj.magic | grep -o Obj.magic | wc -l should give 0

Currently it gives 87 on the 8.8+alpha branch!

Automatic proof fails for program with "with" on an existing variable

The handling of the refine/with construct is incorrect in the automatic eliminator proof, the [set(refine:=domain)] certainly does not select the right occurrences to abstract and this results in a non-well-guarded proof.

Require Import Equations.Equations.

Equations Rtuple'' (domain : list Type) : Type :=
  Rtuple'' nil := unit;
  Rtuple'' (cons d ds) <= ds => {
    | nil => d ;
    | _ => prod (Rtuple'' ds) d }.

Next Obligation.
  revert domain. fix 1.
  destruct domain. constructor.
  autorewrite with Rtuple''.
  constructor.
  set(refine:=domain) at 2 4; clearbody refine. destruct refine.
  simpl. constructor. simpl. constructor.
  apply Rtuple''_ind_fun_obligation.
Defined.

Anomaly

Require Import Equations.Equations.

Equations Rtuple' (domain : list Type) : Type :=
  Rtuple' nil := unit;
  Rtuple' (cons d nil) := d;
  Rtuple' (cons d ds) := prod (Rtuple' ds) d.

outputs:

Error: Conversion test raised an anomaly

[refman] nitpicking on identity function

In the manual (equations_intro.v) the following function is called "identity":

(**
...
The simplest example of this is using the [lt] order on natural numbers
    to define a recursive definition of identity: *)

Equations id (n : nat) : nat :=
  id n by rec n lt :=
  id 0 := 0;
  id (S n') := id n'.

I would call it contrived_zero, because it always returns O.

Equations handles certain overlapping patterns incorrectly.

The following example:

From Coq.Lists Require Import List.
From Equations Require Import Equations.

(* This type is from VST: https://github.com/PrincetonUniversity/VST/blob/v2.1/floyd/compact_prod_sum.v#L6 *)
Fixpoint compact_prod (T: list Type): Type :=
  match T with
  | nil => unit
  | t :: nil => t
  | t :: T0 => (t * compact_prod T0)%type
  end.

(* The rest is a nonsensical, just to give a minimalistic reproducible example *)
Inductive foo :=
| Nat : foo
| List : foo.

Definition foo_type (f:foo) : Type :=
  match f with
  | Nat => nat
  | List => list unit
  end.

Equations num (f:foo) (val:foo_type f) : nat := {
  num Nat val := val;
  num List val := length val }
(* Using "where" instead of a separate Equations here because of Issue #73 - want to specify explicit (struct ts) here and it only works with "where" *)
where (struct fs) sum (fs : list foo) (val: compact_prod (map foo_type fs)) : nat := {
  sum nil _ := 0;
  sum (cons f nil) val := num f val;
  sum (cons f tl) val := num f (fst val) + sum tl (snd val)}.

results in the following error:

Recursive definition of sum is ill-formed.
In environment
num : forall f : foo, foo_type f -> nat
f : foo
val : foo_type f
sum : forall fs : list foo, compact_prod (map foo_type fs) -> nat
fs : list foo
val0 : compact_prod (map foo_type fs)
f0 : foo
l : list foo
val1 : compact_prod (map foo_type (f0 :: l))
f1 : foo
l0 : list foo
val2 : compact_prod (map foo_type (f0 :: f1 :: l0))
Recursive call to sum has principal argument equal to "f1 :: l0" instead of one of the following variables: 
"l" "l0".
Recursive definition is:
"fun (fs : list foo) (val : compact_prod (map foo_type fs)) => sum_functional num sum fs val".

Fatal error: out of memeory

Hi,
coqc (version 8.7.2 with coq-equations 1.0+8.7
on Ubuntu Linux 16.04) tries for about 10 minutes
and finally dies with "Fatal error: out of memory" on this:

Require Import Fin.
From Equations Require Import Equations.

(* crashes Coq *)
Equations invertFin {n : nat} (x : Fin.t n) : Fin.t n :=
invertFin {n:=0} x           :=! x;
invertFin {n:=(S 0)}     F1  := F1;
invertFin {n:=(S (S n))} F1  := FS (invertFin F1);
invertFin {n:=(S (S n))} (FS x) <= invertFin x => {
                                | F1      := F1;
                                | (FS ix) := _}.

Strange, isn't it?
Best regards,
Tim

Incompatibility with MathComp due to notation levels.

When trying to load mathcomp.ssreflect.ssrfun after Equations.Equations, I get the following error:

Error: Notation _ .1 is already defined at level 3 with arguments at next level while it is now required to be at level 2 with arguments at level 2.

Loading the libraries in reverse order of course yields the reverse error message. As far as I am concerned, this makes the package incompatible with MathComp. I suppose it's unlikely that MathComp is going to change this, so I hope it can be changed in Equations. There are likely further clashes, at the very least "_.2".

Implicit Arguments of Constructors in Patterns

The multiple possible ways to give arguments to constructors are a bit confusing to me.

From Equations Require Import Equations.
Require Vector. 
 Equations test {X n} (v : vector X (S n)) : vector X 0 :=
    {
      test Vector.cons := Vector.nil
    }.

  Equations test1 {X n} (v : vector X (S n)) : vector X n :=
    {
      test1 (Vector.cons a) := a
    }.

  Equations test2 {X n} (v : vector X (S n)) : vector X n :=
    {
      test2 (Vector.cons n a) := a
    }.

  Equations test3 {X n} (v : vector X (S n)) : vector X n :=
    {
      test3 (Vector.cons X n a) := a
    }.

Derive Subterm fails with uncaught exception Not_found

Inductive TupleT : nat -> Type :=
nilT : TupleT 0
| consT {n} (A : Set) : (A -> TupleT n) -> TupleT (S n).

Require Import Equations.

Inductive Tuple : forall {n}, TupleT n -> Type :=
nil : Tuple nilT
| cons {n} (A : Set) (x : A) (F : A -> TupleT n) : Tuple (F x) -> Tuple (consT A F).

Inductive TupleMap : forall n, TupleT n -> TupleT n -> Type :=
tmNil : TupleMap _ nilT nilT
| tmCons {n} {A B : Set} (F : A -> TupleT n) (G : B -> TupleT n)
: (forall x, sigT (fun y => TupleMap _ (F x) (G y))) -> TupleMap _ (consT A F) (consT B G).

Derive Subterm for TupleMap.

(* Anomaly: uncaught exception Not_found. Please report. *)

Installation failure (Unbound value Array.for_all)

I am still mostly ignorant about OPAM and Coq packages, so maybe I am just doing something stupid…

$ opam install coq-equations
The following actions will be performed:
  - install coq-equations 1.0~beta

=-=- Gathering sources =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
[coq-equations] Archive in cache

=-=- Processing actions -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
[ERROR] The compilation of coq-equations failed at "make -j4".
Processing  1/1: [coq-equations: rm]
#=== ERROR while installing coq-equations.1.0~beta ============================#
# opam-version 1.2.2
# os           linux
# command      make -j4
# path         /home/jojo/.opam/system/build/coq-equations.1.0~beta
# compiler     system (4.02.3)
# exit-code    2
# env-file     /home/jojo/.opam/system/build/coq-equations.1.0~beta/coq-equations-31322-e7966f.env
# stdout-file  /home/jojo/.opam/system/build/coq-equations.1.0~beta/coq-equations-31322-e7966f.out
# stderr-file  /home/jojo/.opam/system/build/coq-equations.1.0~beta/coq-equations-31322-e7966f.err
### stdout ###
# [...]
# CAMLC -c src/simplify.ml
# CAMLC -c src/splitting.ml
# CAMLC -c src/principles_proofs.ml
# CAMLC -c src/principles.mli
# CAMLC -pp -c src/g_equations.ml4
# CAMLOPT -c src/covering.ml
# CAMLC -c src/principles.ml
# Makefile:523: recipe for target 'src/principles.cmo' failed
# Axioms:
# A : Set
### stderr ###
# [...]
# findlib: [WARNING] Interface derive.cmi occurs in several directories: /home/jojo/.opam/system/lib/coq/plugins/derive, src
# findlib: [WARNING] Interface derive.cmi occurs in several directories: /home/jojo/.opam/system/lib/coq/plugins/derive, src
# findlib: [WARNING] Interface derive.cmi occurs in several directories: /home/jojo/.opam/system/lib/coq/plugins/derive, src
# findlib: [WARNING] Interface derive.cmi occurs in several directories: /home/jojo/.opam/system/lib/coq/plugins/derive, src
# findlib: [WARNING] Interface derive.cmi occurs in several directories: /home/jojo/.opam/system/lib/coq/plugins/derive, src
# findlib: [WARNING] Interface derive.cmi occurs in several directories: /home/jojo/.opam/system/lib/coq/plugins/derive, src
# File "src/principles.ml", line 1032, characters 4-17:
# Error: Unbound value Array.for_all
# make: *** [src/principles.cmo] Error 2
# make: *** Waiting for unfinished jobs....



=-=- Error report -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
The following actions failed
  - install coq-equations 1.0~beta
No changes have been performed

Notations do not always work in pattern-matching

The following snippet produces an error message.

Require Import Coq.Lists.List.
Import ListNotations.
From Equations Require Import Equations.

Equations app {A} (l l' : list A) : list A :=
app [] l' := l' ;                                  (* <- here notations work *)
app (a :: l) l' := a :: (app l l').

The error message is

Error: Syntax error: ')' expected after [lpatt] (in [patt]).

It works if I change (a :: l) with cons a l.

Tested with Coq 8.8.0, Equations 1.0, both installed via OPAM.

Silly replicate function on vectors

The following piece of code returns an error:

From Coq Require Import Vector.
From Equations Require Import Equations.

Fail Equations silly_replicate {A} (n : nat) (x : A) : Vector.t A n :=
silly_replicate O _ := nil;
silly_replicate (S n') x <= (silly_replicate n' x) := {
  | nil => cons x nil;
  | cons h tl => cons x (cons h tl)
}.

Here is the error message:

In environment
silly_replicate :
let H := fixproto in forall (A : Type) (n : nat), A -> vector A n
A1 : Type
h : nat
x : A1
wildcard : A1
tl : vector A1 h
The term "tl" has type "vector A1 h" while it is expected to have type
 "vector nat ?n0" (cannot unify "A1" and "nat").

However, if I don't name the components of cons, then it works:

Equations silly_replicate {A} (n : nat) (x : A) : Vector.t A n :=
silly_replicate O _ := nil;
silly_replicate (S n') x <= (silly_replicate n' x) := {
  | nil => cons x nil;
  | cons _ _ => cons x (cons _ _)
}.

Also, both definitions work for lists.

Equations no longer compiles against current trunk / v8.3

The source file equations.ml fails to compile due to changes in the API of the Constrintern module.

(struct id) option on Equations seems to be silently ignored.

Using a contrived example to show the issue:

From Coq.Lists Require Import List.
From Equations Require Import Equations.

Equations (struct l1) zip {A} {B} (l1 : list A) (l2 : list B) : list (A*B) :=
zip (cons h1 t1) (cons h2 t2) := (h1,h2) :: zip t1 t2;
zip _ _ := nil.

Equations (struct l2) zip2 {A} {B} (l1 : list A) (l2 : list B) : list (A*B) :=
zip2 (cons h1 t1) (cons h2 t2) := (h1,h2) :: zip2 t1 t2;
zip2 _ _ := nil.

Print zip.
Print zip2.

both zip and zip2 end up being identically defined. This is with Coq 8.7.2 and coq-equations 1.0+8.7 installed using opam with 4.06.0 OCaml.

Anomaly when printing function created by Equations

With the coq-trunk branch,

Inductive TupleT : nat -> Type :=
nilT : TupleT 0
| consT {n} A : (A -> TupleT n) -> TupleT (S n).

Require Import Equations.

Equations constTupleT (A : Type) n : TupleT n :=
constTupleT A (S _) := consT A (const (constTupleT A _));
constTupleT _ _     := nilT.

Print constTupleT.

prints

constTupleT = 
fix constTupleT (A : Type) (n : nat) {struct n} : constTupleT_comp A n :=
  match n as n0 return (@block Type (constTupleT_comp A n0)) withAnomaly: File "parsing/ppconstr.ml", line 181, characters 6-12: Assertion failed.
Please report.

Problem with recursion

The following code gives me:

Anomaly "Uncaught exception Not_found."

Am I doing something wrong here?

Require Import Coq.Vectors.Vector.
Require Import Coq.PArith.PArith.

Require Import Equations.Equations.
Require Import Equations.EqDec.
Unset Equations WithK.

Generalizable All Variables.

Definition obj_idx : Type := positive.
Definition arr_idx (n : nat) : Type := Fin.t n.

Import VectorNotations.

Definition obj_pair := (obj_idx * obj_idx)%type.

Inductive Term {a} (tys : Vector.t (obj_idx * obj_idx) a)
          : obj_idx -> obj_idx -> Type :=
  | Ident : forall dom, Term tys dom dom
  | Morph (f : arr_idx a) : Term tys (fst (tys[@f])) (snd (tys[@f]))
  | Comp (dom mid cod : obj_idx)
         (f : Term tys mid cod) (g : Term tys dom mid) :
      Term tys dom cod.

Arguments Ident {a tys dom}.
Arguments Morph {a tys} f.
Arguments Comp {a tys dom mid cod} f g.

Derive Subterm for Term.

Fixpoint term_size
         {a : nat} {tys : Vector.t obj_pair a}
         {dom cod} (t : @Term a tys dom cod) : nat :=
  match t with
  | Ident    => 1%nat
  | Morph _  => 1%nat
  | Comp f g => 1%nat + term_size f + term_size g
  end.

Equations comp_assoc_simpl_rec {a : nat} {tys dom cod}
          (t : @Term a tys dom cod) : @Term a tys dom cod :=
  comp_assoc_simpl_rec t by rec t (MR lt (@term_size a tys dom cod)) :=
  comp_assoc_simpl_rec (Comp f g) <= comp_assoc_simpl_rec f => {
    | Comp i j => Comp i (comp_assoc_simpl_rec (Comp j g));
    | x => Comp x (comp_assoc_simpl_rec g)
  };
  comp_assoc_simpl_rec x := x.

Ability to drop names in the type declaration of a function

I'd like to be able to define functions like so:

From Coq Require Import List.
From Equations Require Import Equations.

Equations app {A} : list A -> list A -> list A :=
app xs ys := fold_right cons ys xs.

but it fails with the following error message:

Non-exhaustive pattern-matching, no clause found for:
app A
In context:
A : Type

Is there a workaround?

Feature request: allow placeholders in the type of functions

Hi,

I'm trying to switch from Program Fixpoint to Equations, and so far I'm happy with the rewrite capabilities provided by Equations for unfolding recursive calls.

On the other hand, Program Fixpoint allowed leaving holes in the types of the functions themselves, while Equations doesn't. Are there any plans to add this feature?

Require Equations.Equations.

Definition f (l l': list nat) (H: 0 = 0): Prop. Admitted.

Equations id (l: list nat) (H: f l l _): { r: list nat | f l r _ } :=
  id l H := exist _ nil _.

Cannot infer this placeholder of type [...]

My workaround for now is to define the type of Equations beforehand, using the usual Program Definition. Is there a better way?

Require Equations.Equations.

Definition f (l l': list nat) (H: 0 = 0): Prop. Admitted.

Program Definition id_arg2 l: Type := f l l _.
Program Definition id_return_type (l: list nat) (H: id_arg2 l): Type := { r: list nat | f l r _ }.

Equations id (l: list nat) (H: id_arg2 l): id_return_type l H :=
  id l H := exist _ nil _.

Another question I have is whether Equations can also support automatic translations (through the generation of additional Obligations) between types and their refine counter-parts (to avoid having to write exist _ nil _), as Program does?

Section "cooking" kills opaqueness for reduction

If I define the following function at the top level, it's opaque for reduction, just as the manual says.

From Equations Require Import Equations.

Equations id {A} (x : A) : A :=
id x := x.
About id.
(* id is basically transparent but considered opaque for reduction *)

However, if I define a function in a section, then outside the section it's transparent:

From Equations Require Import Equations.

Section CookingKillsOpaquenessForReduction.
Equations id {A} (x : A) : A :=
id x := x.
About id.
(* id is basically transparent but considered opaque for reduction *)
End CookingKillsOpaquenessForReduction.

About id.
(* id' is transparent *)

Fix compiler warnings

Dear Equations devs, as it is today, compiling the master version of the plugin produces quite a few deprecated warnings due to Coq API changes.

It would be really appreciated if you could fix those, it is usually trivial to do so as the deprecation message should indicate what has to be done.

Anomaly "Helper not found while proving induction lemma."

The following code

From Coq.Lists Require Import List.
From Equations Require Import Equations.

(* This type is from VST: https://github.com/PrincetonUniversity/VST/blob/v2.1/floyd/compact_prod_sum.v#L6 *)
Fixpoint compact_prod (T: list Type): Type :=
  match T with
  | nil => unit
  | t :: nil => t
  | t :: T0 => (t * compact_prod T0)%type
  end.

(* The rest is a nonsensical, just to give a minimalistic reproducible example *)
Inductive foo :=
| Nat : foo -> nat -> foo
| List : list foo -> foo.

Equations foo_type (ft:foo) : Type :=
  foo_type (Nat f _) := foo_type f;
  foo_type (List fs) := compact_prod (List.map foo_type fs).

(* val was moved into the result type, rather than being an argument, to work around issues #73 and #85 *)
Equations sum (fx:foo) : forall (val:foo_type fx), nat := {
  sum (Nat f _) := sum f;
  sum (List ff) := fun val => sum_list ff val }

where sum_list (fs : list foo) : forall (vval: compact_prod (map foo_type fs)), nat := {
  sum_list nil := fun vval => 0;
  (* The "with clause" below is there to work around issue #78 *)
  sum_list (cons hd tl) <= fun val1 => sum_list tl val1 => {
    sum_list (cons hd nil) _ := fun vval => sum hd vval;
    sum_list (cons hd _) sumtl := fun vval => sum hd (fst vval) + sumtl (snd vval)}}.

results in:

fix/cofix without a name are deprecated, please use the named version. [nameless-fix,deprecated]
Induction principle could not be proved automatically: 
Anomaly "Helper not found while proving induction lemma." Please report at http://coq.inria.fr/bugs/.

P.S. if I eta-expand the first equation into sum (Nat f _) := fun val => sum f val then I get Illegal application error along the lines of issue #84 instead...

Slowness in the simp tactic (5s to complete)

Very likely to be related to (coq/coq#7585).

In this multifile project, using simp transport in * takes 5s to complete.

Removing the line transport t T by rec 0 lt := makes the problem disappear, and putting all the code in the same file also makes the problem disappear. (the rewrite then takes 0.001s).

Zip file of the project: simp-slowness.zip

File1.v

Require Import Equations.Equations.
Require Import Omega.

Inductive type: Set :=
  | T_bool: type
  | T_prod: type -> type -> type.

Equations transport (t: nat) (T: type): Prop :=
  transport t T by rec 0 lt :=

  transport t T_bool := True;

  transport t (T_prod U V) :=
    transport t U /\
    transport t V.

Next Obligation. Admitted.
Next Obligation. Admitted.

(* obligation generated for transport_ind_fun *)
Next Obligation.
  generalize t.
  induction T; repeat intuition || simp transport in *.
Defined.

File2.v

Require Import Top.File1.
Require Import Omega.
Require Import Equations.Equations.

Lemma l:
  forall T t,
    transport t T ->
    forall t',
      transport t' T.
Proof.
  induction T; intuition auto; try omega.
  - Set Ltac Profiling.
    simp transport in *.
Abort.

Equations hides definitions from Init.

This is probably more an issue of Program but Requiring Equations has an unpleasant side-effect which breaks existing code: it hides Init.Wf.Fix_eq with its own definition of Wf.Fix_eq.

Since Init is implicitely imported in the scope, a user might take some time to understand and fix the issue (namely by rewriting its Fix_eq occurrences to Init.Wf.Fix_eq).

Coq Anomaly using "with" construct

Hi,

at the very end the code below gives this Coq warning:

Induction principle could not be proved automatically: 
Anomaly
"File "src/principles.ml", line 433, characters 16-22: Assertion failed." 
Please report at http://coq.inria.fr/bugs/.

I quite often encounter this warning when trying to use "with". Do I do
something wrong? Should I rather report it in the Coq list (as it says)?

Best,
Tim

Require Import Fin.
From Equations Require Import Equations.
Set Equations Transparent.

Equations FL (n : nat) : Fin.t (S n) :=
  FL 0     := F1;
  FL (S n) := FS (FL n).

Equations FU {n : nat} (x : Fin.t n) : Fin.t (S n) :=
  FU F1     := F1;
  FU (FS x) := FS (FU x).

Equations invertFin {n : nat} (x : Fin.t n) : Fin.t n :=
  invertFin  F1    := FL _;
  invertFin (FS x) := FU (invertFin x).

Equations invFULemma {n : nat} (x : Fin.t n) :
                     invertFin (FU x) = FS (invertFin x) :=
  invFULemma F1     := _;
  invFULemma (FS x) := (f_equal _ (invFULemma x)).

Equations invFLLemma (n : nat) : invertFin (FL n) = F1 :=
  invFLLemma 0     := eq_refl;
  invFLLemma (S n) := (f_equal _ (invFLLemma n)).

Equations invertFinInv {n : nat} (x : Fin.t n) :
                       invertFin (invertFin x) = x :=
  invertFinInv {n:=0}      x     :=! x;
  invertFinInv {n:=(S _)}  F1    := (invFLLemma _);
  invertFinInv {n:=(S _)} (FS y) := (eq_trans
                                     (invFULemma (invertFin y))
                                     (f_equal _ (invertFinInv y))).

Definition invFinViewType {n : nat} (x : (Fin.t n)) : Type :=
  { y : Fin.t n & x = invertFin y }.

Definition invFinView {n : nat} (x : (Fin.t n)) : invFinViewType x :=
  existT _ (invertFin x) (eq_sym (invertFinInv x)).

Equations finFUOrFL {n : nat} (x : Fin.t (S n)) :
                    { y : Fin.t n & x = FU y } + ( x = FL n ) :=
  finFUOrFL  {n:=0}     F1                     := (inr eq_refl);
  finFUOrFL  {n:=(S _)} x <= invFinView x => {
                          | (existT F1 eq)     := (inr eq);
                          | (existT (FS _) eq) := (inl (existT _ (invertFin _) eq))}.

Unexpected obligation generated for *_ind_fun

In this example, an obligation in generated for transport_ind_fun, which is not solved automatically.

Require Import Equations.Equations.

Inductive type: Set :=
  | T_bool: type
  | T_prod: type -> type -> type.

Equations transport (t: nat) (T: type): Prop :=
  transport t T by rec 0 lt :=

  transport t T_bool := True;

  transport t (T_prod U V) :=
    transport t U /\
    transport t V.

Next Obligation. Admitted.
Next Obligation. Admitted.

(* obligation generated for transport_ind_fun *)
Next Obligation.
  induction T; repeat intuition || simp transport in *.
Defined.

Deprecated `coq_makefile` features

Running coq_makefile -f _CoqProject -o Makefile produces:

Warning: -extra and -extra-phony are deprecated.
Warning: Write the extra targets in Makefile.local.

Equations lemma takes a long time to prove

The Admit in the end takes 30 seconds to go through. Apparently it is due to lemma  `foldLeft_unfold_eq' taking a while to prove. (thanks to the people on the coq IRC channel)

Removing (l: List T) from either f_type or foldLeft_type makes the Admit go through quite fast.
Replacing Cons_type with List as well.

Require Equations.Equations.

Set Program Mode.

Definition ifthenelse b A (e1: true = b -> A) (e2: false = b -> A): A. Admitted.
  
Definition List (T: Type): Type. Admitted.
Definition isCons (T: Type) (src: List T): bool. Admitted.
Definition Cons_type (T: Type): Type := {src: List T | (isCons T src = true)}.
Definition head (T: Type) (src: Cons_type T): T. Admitted.
Definition tail (T: Type) (src: Cons_type T): List T. Admitted.
Definition f_type (T R: Type) (l: List T): Type := R -> (T -> R).
Definition foldLeft_type (T R: Type) (l: List T): Type := R.

Equations foldLeft (T R: Type) (l: List T) (z: R) (f: f_type T R l): foldLeft_type T R l := 
foldLeft T R l z f by rec 0 lt :=
foldLeft T R l z f :=
  ifthenelse (isCons _ l) R
             (fun _ => foldLeft T R (tail T l) (f z (head T l)) f)
             (fun _ => z).

Admit Obligations.

Unable to build Coq-Equations

We're having trouble building Coq-Equations:

$ ocaml -version
The Objective Caml toplevel, version 3.12.1

$ camlp4 -version
3.12.1

$ camlp5 -v
Camlp5 version 6.05 (ocaml 3.12.1)

$ make -version
GNU Make 3.82
Built for x86_64-unknown-linux-gnu

$ coqc -v
The Coq Proof Assistant, version 8.3pl4 (April 2012)
compiled on Apr 10 2012 22:08:24 with OCaml 3.12.1

On branch master:

$ make
...
*** Warning: in file theories/Init.v, declared ML module equations_plugin has not been found !
ocamlopt.opt -c -rectypes -I src -I /usr/lib/coq/kernel -I /usr/lib/coq/lib -I /usr/lib/coq/library -I /usr/lib/coq/parsing -I /usr/lib/coq/pretyping -I /usr/lib/coq/interp -I /usr/lib/coq/proofs -I /usr/lib/coq/tactics -I /usr/lib/coq/toplevel -I /usr/lib/coq/plugins/cc -I /usr/lib/coq/plugins/dp -I /usr/lib/coq/plugins/extraction -I /usr/lib/coq/plugins/field -I /usr/lib/coq/plugins/firstorder -I /usr/lib/coq/plugins/fourier -I /usr/lib/coq/plugins/funind -I /usr/lib/coq/plugins/groebner -I /usr/lib/coq/plugins/interface -I /usr/lib/coq/plugins/micromega -I /usr/lib/coq/plugins/nsatz -I /usr/lib/coq/plugins/omega -I /usr/lib/coq/plugins/quote -I /usr/lib/coq/plugins/ring -I /usr/lib/coq/plugins/romega -I /usr/lib/coq/plugins/rtauto -I /usr/lib/coq/plugins/setoid_ring -I /usr/lib/coq/plugins/subtac -I /usr/lib/coq/plugins/subtac/test -I /usr/lib/coq/plugins/syntax -I /usr/lib/coq/plugins/xml -I /usr/lib/ocaml/camlp5 -pp ""camlp5"o -I /usr/lib/ocaml -I . -I /usr/lib/coq/kernel -I /usr/lib/coq/lib -I /usr/lib/coq/library -I /usr/lib/coq/parsing -I /usr/lib/coq/pretyping -I /usr/lib/coq/interp -I /usr/lib/coq/proofs -I /usr/lib/coq/tactics -I /usr/lib/coq/toplevel -I /usr/lib/coq/plugins/cc -I /usr/lib/coq/plugins/dp -I /usr/lib/coq/plugins/extraction -I /usr/lib/coq/plugins/field -I /usr/lib/coq/plugins/firstorder -I /usr/lib/coq/plugins/fourier -I /usr/lib/coq/plugins/funind -I /usr/lib/coq/plugins/groebner -I /usr/lib/coq/plugins/interface -I /usr/lib/coq/plugins/micromega -I /usr/lib/coq/plugins/nsatz -I /usr/lib/coq/plugins/omega -I /usr/lib/coq/plugins/quote -I /usr/lib/coq/plugins/ring -I /usr/lib/coq/plugins/romega -I /usr/lib/coq/plugins/rtauto -I /usr/lib/coq/plugins/setoid_ring -I /usr/lib/coq/plugins/subtac -I /usr/lib/coq/plugins/subtac/test -I /usr/lib/coq/plugins/syntax -I /usr/lib/coq/plugins/xml pa_extend.cmo pa_macro.cmo q_MLast.cmo grammar.cma -loc loc -impl" src/equations_common.ml
File "src/equations_common.ml", line 78, characters 54-55:
Error: This expression has type Term.constr option
but an expression was expected of type Term.constr
make: *** [src/equations_common.cmx] Error 2

On branch 8.3:

$ make
...
*** Warning: in file theories/Init.v, declared ML module equations_plugin has not been found !
ocamlopt.opt -c -rectypes -I src -I /usr/lib/coq/kernel -I /usr/lib/coq/lib -I /usr/lib/coq/library -I /usr/lib/coq/parsing -I /usr/lib/coq/pretyping -I /usr/lib/coq/interp -I /usr/lib/coq/proofs -I /usr/lib/coq/tactics -I /usr/lib/coq/toplevel -I /usr/lib/coq/plugins/cc -I /usr/lib/coq/plugins/dp -I /usr/lib/coq/plugins/extraction -I /usr/lib/coq/plugins/field -I /usr/lib/coq/plugins/firstorder -I /usr/lib/coq/plugins/fourier -I /usr/lib/coq/plugins/funind -I /usr/lib/coq/plugins/groebner -I /usr/lib/coq/plugins/interface -I /usr/lib/coq/plugins/micromega -I /usr/lib/coq/plugins/nsatz -I /usr/lib/coq/plugins/omega -I /usr/lib/coq/plugins/quote -I /usr/lib/coq/plugins/ring -I /usr/lib/coq/plugins/romega -I /usr/lib/coq/plugins/rtauto -I /usr/lib/coq/plugins/setoid_ring -I /usr/lib/coq/plugins/subtac -I /usr/lib/coq/plugins/subtac/test -I /usr/lib/coq/plugins/syntax -I /usr/lib/coq/plugins/xml -I /usr/lib/ocaml/camlp5 -pp ""camlp5"o -I /usr/lib/ocaml -I . -I /usr/lib/coq/kernel -I /usr/lib/coq/lib -I /usr/lib/coq/library -I /usr/lib/coq/parsing -I /usr/lib/coq/pretyping -I /usr/lib/coq/interp -I /usr/lib/coq/proofs -I /usr/lib/coq/tactics -I /usr/lib/coq/toplevel -I /usr/lib/coq/plugins/cc -I /usr/lib/coq/plugins/dp -I /usr/lib/coq/plugins/extraction -I /usr/lib/coq/plugins/field -I /usr/lib/coq/plugins/firstorder -I /usr/lib/coq/plugins/fourier -I /usr/lib/coq/plugins/funind -I /usr/lib/coq/plugins/groebner -I /usr/lib/coq/plugins/interface -I /usr/lib/coq/plugins/micromega -I /usr/lib/coq/plugins/nsatz -I /usr/lib/coq/plugins/omega -I /usr/lib/coq/plugins/quote -I /usr/lib/coq/plugins/ring -I /usr/lib/coq/plugins/romega -I /usr/lib/coq/plugins/rtauto -I /usr/lib/coq/plugins/setoid_ring -I /usr/lib/coq/plugins/subtac -I /usr/lib/coq/plugins/subtac/test -I /usr/lib/coq/plugins/syntax -I /usr/lib/coq/plugins/xml pa_extend.cmo pa_macro.cmo q_MLast.cmo grammar.cma -loc loc -impl" src/equations_common.ml
File "src/equations_common.ml", line 77, characters 6-15:
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
(None, _)
File "src/equations_common.ml", line 353, characters 0-299:
Error: Unbound value globwit_hintbases
make: *** [src/equations_common.cmx] Error 2

On branch coq-trunk:

$ make
src/equations_common.ml4:2: *** missing separator. Stop.

It seems there is a problem with files ending in a number being treated as Makefiles.

Online tutorial outdated.

This tutorial:
https://www.irif.fr/~sozeau/research/coq/equations-intro.html
uses

Require Import Equations.

to import Equations while it should be

From Equations Require Import Equations.

(which is a bit weird from a beginner's point of view. I would prefer:

From Equations Require Import All.

or something like that.)

No documentation or example on how to define > 2 mutually recursive functions.

From Coq.Lists Require Import List.
From Equations Require Import Equations.

Inductive foo: Set :=
| Foo1 : list foo -> foo
| Foo2 : list foo -> foo.

Equations f (x: foo) : nat := {
  f (Foo1 l):= aux1 l;
  f (Foo2 l) := aux2 l
}
  where aux1 (l : list foo) : nat := { 
    aux1 [] := 1;
    aux1 (cons hd tl) := f hd + aux1 tl }
  where aux2 (l : list foo) : nat := { 
    aux2 [] := 1;
    aux2 (cons hd tl) := f hd + aux2 tl }.

results in

Illegal application: 
The term "aux1_functional" of type "(foo -> nat) -> (list foo -> nat) -> (list foo -> nat) -> list foo -> nat"
cannot be applied to the terms
 "f" : "foo -> nat"
 "aux1" : "list foo -> nat"
 "l" : "list foo"
The 3rd term has type "list foo" which should be coercible to "list foo -> nat".

This is with Coq 8.7.2 and coq-equations 1.0+8.7 installed using opam with 4.06.0 OCaml.

Variables introduced by pattern matching are not lexical scoped

Equations bug (x : nat) : nat :=
  bug O := O;
  bug (S n) <= 2 => {
   | x <= 3 => {
     | x => x
   }
  }.

Compute bug 5.

This yields 2 instead of 3.

Equations command breaks Write State

If you put a Write State command in after the first Equation in test-suite/Basics.v, like this:

Require Import Program Equations Bvector List.
Require Import Relations.
Require Import DepElimDec.

Module TestF.

Equations f (n : nat) : nat :=
f 0 := 42 ;
f (S m) with f m :=
{
f (S m) IH := _
}.

Next Obligation. exact IH. Defined.
Write State bisect.
End TestF.

you get:

Anomaly: Uncaught exception Invalid_argument("output_value: functional value").
Please report.

Hang after solving obligations

In issue #7 it looks like wrong code is being generated, so I tried without "by rec" instead:

Inductive TupleT : nat -> Type :=
nilT : TupleT 0
| consT {n} A : (A -> TupleT n) -> TupleT (S n).

Require Import Equations.

Ltac wf_subterm := intro;
  simp_exists;
  on_last_hyp depind; split; intros; simp_exists;
    on_last_hyp ltac:(fun H => red in H);
    [ exfalso | ];
    on_last_hyp depind;
    intuition.

Inductive Tuple : forall n, TupleT n -> Type :=
  nil : Tuple _ nilT
| cons {n A} (x : A) (F : A -> TupleT n) : Tuple _ (F x) -> Tuple _ (consT A F).

Inductive TupleMap : forall n, TupleT n -> TupleT n -> Type :=
  tmNil : TupleMap _ nilT nilT
| tmCons {n} {A B} (F : A -> TupleT n) (G : B -> TupleT n)
  : (forall x, sigT (TupleMap _ (F x) ∘ G)) -> TupleMap _ (consT A F) (consT B G).

Derive Signature for TupleMap.

Program Instance TupleMap_depelim n T U : DependentEliminationPackage (TupleMap n T U)
:= { elim_type := ∀ (P : forall n t t0, TupleMap n t t0 -> Type),
   P _ _ _ tmNil ->
  (∀ n A B (F : A -> TupleT n) (G : B -> TupleT n)
    (s : ∀ x, sigT (TupleMap _ (F x) ∘ G))
    (r : ∀ x, P _ _ _ (projT2 (s x))),
    P _ _ _ (tmCons F G s))
  -> ∀ (tm : TupleMap n T U), P _ _ _ tm }.
Next Obligation.
  revert n T U tm.
  fix IH 4.
  intros.
  Ltac destruct' x := destruct x.
  on_last_hyp destruct'; [ | apply X0 ]; auto.
Defined.

(* Doesn't know how to deal with the nested TupleMap 
   Derive Subterm for TupleMap. *)

Inductive TupleMap_direct_subterm
              : ∀ (n : nat) (H H0 : TupleT n) (n0 : nat) 
                (H1 H2 : TupleT n0),
                TupleMap n H H0 → TupleMap n0 H1 H2 → Prop :=
    TupleMap_direct_subterm_0_0 : ∀ (n : nat) (H H0 : TupleT n) 
                                  (n0 : nat) (H1 H2 : TupleT n0) 
                                  (n1 : nat) (H3 H4 : TupleT n1)
                                  (x : TupleMap n H H0)
                                  (y : TupleMap n0 H1 H2)
                                  (z : TupleMap n1 H3 H4),
                                  TupleMap_direct_subterm n H H0 n0 H1 H2 x y
                                  → TupleMap_direct_subterm n0 H1 H2 n1 H3 H4
                                      y z
                                    → TupleMap_direct_subterm n H H0 n1 H3 H4
                                        x z
|   TupleMap_direct_subterm_1_1 : ∀ n {A B} (F : A -> TupleT n) (G : B -> TupleT n)
  (H : forall x, sigT (TupleMap _ (F x) ∘ G)) (x : A),
  TupleMap_direct_subterm _ _ (G (projT1 (H _))) _ _ _ (projT2 (H x)) (tmCons _ _ H).

Definition TupleMap_subterm := 
λ x y : {index : {n : nat & sigT (λ _ : TupleT n, TupleT n)} &
     TupleMap (projT1 index) (projT1 (projT2 index)) (projT2 (projT2 index))},
TupleMap_direct_subterm (projT1 (projT1 x)) (projT1 (projT2 (projT1 x)))
  (projT2 (projT2 (projT1 x))) (projT1 (projT1 y))
  (projT1 (projT2 (projT1 y))) (projT2 (projT2 (projT1 y))) 
  (projT2 x) (projT2 y).

Program Instance WellFounded_TupleMap_subterm : WellFounded TupleMap_subterm.
Solve All Obligations using wf_subterm.

Equations(noind) myComp {n} {B C : TupleT n} (tm1 : TupleMap _ B C) {A : TupleT n} (tm2 : TupleMap _ A B)
: TupleMap _ A C :=
myComp ?(0) ?(nilT) ?(nilT) tmNil ?(nilT) tmNil := tmNil;
myComp ?(S _) ?(consT _ _) ?(consT _ _) (tmCons G H g) (consT _ _) (tmCons F ?(G) f)
:= tmCons _ _ (fun x => existT (fun y => TupleMap _ _ (_ y)) (projT1 (g (projT1 (f x)))) (myComp (projT2 (g (projT1 (f x)))) (projT2 (f x)))).

This hangs after solving the first set of obligations for myComp.

acc_A_B_lexprod is opaque and this blocks evaluation

We cannot compute with Ackermann's function (see e.g. ack.v):

Example test1 : ack (1, 2) = 4 := eq_refl.

Here is the error message:

The term "eq_refl" has type "ack (1, 2) = ack (1, 2)"
while it is expected to have type "ack (1, 2) = 4" (cannot unify
"ack (1, 2)" and "4").

Illegal application in ..._ind_1

Yet another issue that seems related, but somewhat distinct. It could be due to the same underlying cause as one or more issues I already reported, but since the symptoms are distinct, I am reporting as a separate issue just in case.

From Coq.Lists Require Import List.
From Equations Require Import Equations.

(* This type is from VST: https://github.com/PrincetonUniversity/VST/blob/v2.1/floyd/compact_prod_sum.v#L6 *)
Fixpoint compact_prod (T: list Type): Type :=
  match T with
  | nil => unit
  | t :: nil => t
  | t :: T0 => (t * compact_prod T0)%type
  end.

(* The rest is a nonsensical, just to give a minimalistic reproducible example *)
Inductive foo :=
| Nat : foo
| List : list foo -> foo.

Fixpoint foo_type (f:foo) : Type :=
  match f with
  | Nat => nat
  | List fs => compact_prod (map foo_type fs)
  end.

Equations num (f:foo) : forall (val:foo_type f), nat := {
  num Nat := fun val => val;
  num (List nil) := fun val => 0;
  num (List (cons hd tl)) := sum hd (num hd) tl }
where (struct fs) sum (f:foo) (numf: (foo_type f -> nat)) (fs : list foo) (val: compact_prod (map foo_type (f::fs))) : nat := {
  sum f numf nil val := numf val;
  sum f numf (cons hd tl) val := numf (fst val) + sum hd (num hd) tl (snd val)}.

results in

The term "num_ind_1" of type
 "forall f : foo, (foo_type f -> nat) -> forall fs : list foo, compact_prod (map foo_type (f :: fs)) -> nat -> Prop"
cannot be applied to the terms
 "f" : "foo"
 "num f" : "foo_type f -> nat"
 "l" : "list foo"
 "sum f (num f) l" : "compact_prod (map foo_type (f :: l)) -> nat"
The 4th term has type "compact_prod (map foo_type (f :: l)) -> nat" which should be coercible to
 "compact_prod (map foo_type (f :: l))".

Note that this test case is almost identical to the one in issue #84 - the only difference is that there the num (List (cons hd tl)) equation had it rhs eta-expanded.

Problem with coq-equations installation

I have very little knowledge about how to install packages, so I just followed the directions on how to install coq-equation on my mac (I have High Sierra), and I got the following problem:

bash-3.2$ opam install coq-equations.1.0+8.7
The following actions will be performed:
∗ install camlp5 7.05 [required by coq]
∗ install conf-m4 1 [required by ocamlfind]
∗ install ocamlfind 1.7.3-1 [required by coq]
∗ install num 1.1 [required by coq]
∗ install coq 8.7.2 [required by coq-equations]
∗ install coq-equations 1.0+8.7
===== ∗ 6 =====
Do you want to continue ? [Y/n] Y

=-=- Gathering sources =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= 🐫
[coq-released] https://coq.inria.fr/opam/released/archives/coq-equations.1.0+8.7+opam.tar.gz downloaded
[default] https://opam.ocaml.org/archives/num.1.1+opam.tar.gz downloaded
[default] https://opam.ocaml.org/archives/camlp5.7.05+opam.tar.gz downloaded
[default] https://opam.ocaml.org/archives/ocamlfind.1.7.3-1+opam.tar.gz downloaded
[default] https://opam.ocaml.org/archives/coq.8.7.2+opam.tar.gz downloaded

=-=- Processing actions -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= 🐫
∗ installed camlp5.7.05
∗ installed conf-m4.1
∗ installed ocamlfind.1.7.3-1
∗ installed num.1.1
∗ installed coq.8.7.2
[ERROR] The compilation of coq-equations failed at "make -j1".
Processing 6/6: [coq-equations: rm]
#=== ERROR while installing coq-equations.1.0+8.7 =============================#

opam-version 1.2.2

os darwin

command make -j1

path /Users/giannini/.opam/4.06.1/build/coq-equations.1.0+8.7

compiler 4.06.1

exit-code 2

env-file /Users/giannini/.opam/4.06.1/build/coq-equations.1.0+8.7/coq-equations-88650-5788a7.env

stdout-file /Users/giannini/.opam/4.06.1/build/coq-equations.1.0+8.7/coq-equations-88650-5788a7.out

stderr-file /Users/giannini/.opam/4.06.1/build/coq-equations.1.0+8.7/coq-equations-88650-5788a7.err

stdout

[...]

CAMLDEP src/principles_proofs.ml

CAMLDEP src/splitting.ml

CAMLDEP src/covering.ml

CAMLDEP src/syntax.ml

CAMLDEP src/depelim.ml

CAMLDEP src/eqdec.ml

CAMLDEP src/subterm.ml

CAMLDEP src/sigma_types.ml

CAMLDEP src/derive.ml

CAMLDEP src/equations_common.ml

stderr

[...]

/bin/sh: /opt/local/bin/ocamlfind: No such file or directory

/bin/sh: /opt/local/bin/ocamlfind: No such file or directory

/bin/sh: /opt/local/bin/ocamlfind: No such file or directory

/bin/sh: /opt/local/bin/ocamlfind: No such file or directory

/bin/sh: /opt/local/bin/ocamlfind: No such file or directory

/bin/sh: /opt/local/bin/ocamlfind: No such file or directory

/bin/sh: /opt/local/bin/ocamlfind: No such file or directory

/bin/sh: /opt/local/bin/ocamlfind: No such file or directory

/bin/sh: /opt/local/bin/ocamlfind: No such file or directory

Makefile:703: *** "Cannot find the 'ocamlfind' binary used to build Coq (/opt/local/bin/ocamlfind). Pre-compiled binary packages of Coq do not support compiling plugins this way. Please download the sources of Coq and run the Windows build script.". Stop.

=-=- Error report -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= 🐫
The following actions failed
∗ install coq-equations 1.0+8.7
The following changes have been performed
∗ install camlp5 7.05
∗ install conf-m4 1
∗ install coq 8.7.2
∗ install num 1.1
∗ install ocamlfind 1.7.3-1

The former state can be restored with:
opam switch import "~/.opam/4.06.1/backup/state-20180311085727.export"
bash-3.2$

can you tell me what to do? Paola

Obligation tactic not used when declaring an Equation

Tactic t can solve (unsoundly) the goal generated by content, but the obligation remains after the declaration of Equation. Am I missing something to specify that goals should be solved automatically using t?

On the final line, when I do Next Obligation, tactic t is used automatically and the goal is solved.

Require Equations.Equations.

Axiom unsupported: False. 
Axiom ignore_termination: nat.  

Ltac t := intros; match goal with
  | |- (?T < ?T)%nat =>
    unify T ignore_termination; apply False_ind; exact unsupported
  end.

Obligation Tactic := t.

Equations content (n: nat): nat := 
content n by rec ignore_termination lt :=
content n := content n.

Next Obligation. Qed. (* succeeds *)

Variable defined by "where" sometimes "not found in the current environment"

In attempting to work around issue #78 as follows:

From Coq.Lists Require Import List.
From Equations Require Import Equations.

(* This type is from VST: https://github.com/PrincetonUniversity/VST/blob/v2.1/floyd/compact_prod_sum.v#L6 *)
Fixpoint compact_prod (T: list Type): Type :=
  match T with
  | nil => unit
  | t :: nil => t
  | t :: T0 => (t * compact_prod T0)%type
  end.

(* The rest is a nonsensical, just to give a minimalistic reproducible example *)
Inductive foo :=
| Nat : foo
| List : foo.

Definition foo_type (f:foo) : Type :=
  match f with
  | Nat => nat
  | List => list unit
  end.

Equations num (f:foo) (val:foo_type f) : nat :=
  num Nat val := val;
  num List val := length val.

Equations sum (fs : list foo) (val: compact_prod (map foo_type fs)) : nat := {
  sum nil _ := 0;
  sum (cons f tl) val := sum_aux f tl val }
where (struct fs) sum_aux (f:foo) (fs : list foo) (val: compact_prod (map foo_type (f::fs))) : nat := {
  sum_aux f nil val := num f val;
  sum_aux f (cons hd tl) val := num f (fst val) + sum_aux hd tl (snd val)}.

I got The variable sum_aux was not found in the current environment. for the occurrence of sum_aux in the 2nd equation for sum.

P.S. I was actually intending to create a small test case for another error I am getting in trying to work around issue #78 in my actual development, but this issue made it hard to reproduce the other one.

Contexts do not agree for composition

With coq-trunk, this:

Inductive TupleT : nat -> Type :=
nilT : TupleT 0
| consT {n} A : (A -> TupleT n) -> TupleT (S n).

Require Import Equations.

Ltac wf_subterm := intro;
  simp_exists;
  on_last_hyp depind; split; intros; simp_exists;
    on_last_hyp ltac:(fun H => red in H);
    [ exfalso | ];
    on_last_hyp depind;
    intuition.

Inductive Tuple : forall n, TupleT n -> Type :=
  nil : Tuple _ nilT
| cons {n A} (x : A) (F : A -> TupleT n) : Tuple _ (F x) -> Tuple _ (consT A F).

Inductive TupleMap : forall n, TupleT n -> TupleT n -> Type :=
  tmNil : TupleMap _ nilT nilT
| tmCons {n} {A B} (F : A -> TupleT n) (G : B -> TupleT n)
  : (forall x, sigT (TupleMap _ (F x) ∘ G)) -> TupleMap _ (consT A F) (consT B G).

Derive Signature for TupleMap.

Program Instance TupleMap_depelim n T U : DependentEliminationPackage (TupleMap n T U)
:= { elim_type := ∀ (P : forall n t t0, TupleMap n t t0 -> Type),
   P _ _ _ tmNil ->
  (∀ n A B (F : A -> TupleT n) (G : B -> TupleT n)
    (s : ∀ x, sigT (TupleMap _ (F x) ∘ G))
    (r : ∀ x, P _ _ _ (projT2 (s x))),
    P _ _ _ (tmCons F G s))
  -> ∀ (tm : TupleMap n T U), P _ _ _ tm }.
Next Obligation.
  revert n T U tm.
  fix IH 4.
  intros.
  Ltac destruct' x := destruct x.
  on_last_hyp destruct'; [ | apply X0 ]; auto.
Defined.

(* Doesn't know how to deal with the nested TupleMap 
   Derive Subterm for TupleMap. *)

Inductive TupleMap_direct_subterm
              : ∀ (n : nat) (H H0 : TupleT n) (n0 : nat) 
                (H1 H2 : TupleT n0),
                TupleMap n H H0 → TupleMap n0 H1 H2 → Prop :=
    TupleMap_direct_subterm_0_0 : ∀ (n : nat) (H H0 : TupleT n) 
                                  (n0 : nat) (H1 H2 : TupleT n0) 
                                  (n1 : nat) (H3 H4 : TupleT n1)
                                  (x : TupleMap n H H0)
                                  (y : TupleMap n0 H1 H2)
                                  (z : TupleMap n1 H3 H4),
                                  TupleMap_direct_subterm n H H0 n0 H1 H2 x y
                                  → TupleMap_direct_subterm n0 H1 H2 n1 H3 H4
                                      y z
                                    → TupleMap_direct_subterm n H H0 n1 H3 H4
                                        x z
|   TupleMap_direct_subterm_1_1 : ∀ n {A B} (F : A -> TupleT n) (G : B -> TupleT n)
  (H : forall x, sigT (TupleMap _ (F x) ∘ G)) (x : A),
  TupleMap_direct_subterm _ _ (G (projT1 (H _))) _ _ _ (projT2 (H x)) (tmCons _ _ H).

Definition TupleMap_subterm := 
λ x y : {index : {n : nat & sigT (λ _ : TupleT n, TupleT n)} &
     TupleMap (projT1 index) (projT1 (projT2 index)) (projT2 (projT2 index))},
TupleMap_direct_subterm (projT1 (projT1 x)) (projT1 (projT2 (projT1 x)))
  (projT2 (projT2 (projT1 x))) (projT1 (projT1 y))
  (projT1 (projT2 (projT1 y))) (projT2 (projT2 (projT1 y))) 
  (projT2 x) (projT2 y).

Program Instance WellFounded_TupleMap_subterm : WellFounded TupleMap_subterm.
Solve All Obligations using wf_subterm.

Equations(nocomp noind) myComp {n} {B C : TupleT n} (tm1 : TupleMap _ B C) {A : TupleT n} (tm2 : TupleMap _ A B)
: TupleMap _ A C :=
myComp n B C tm1 A tm2 by rec tm1 TupleMap_subterm :=
myComp ?(0) ?(nilT) ?(nilT) tmNil ?(nilT) tmNil := tmNil;
myComp ?(S _) ?(consT _ _) ?(consT _ _) (tmCons G H g) (consT _ _) (tmCons F ?(G) f)
:= tmCons _ _ (fun x => existT (fun y => TupleMap _ _ (_ y)) (projT1 (g (projT1 (f x)))) _).
Next Obligation.
  refine (myComp _ (existT _ _ _) (projT2 (g (projT1 (f x)))) _ _ (projT2 (f x))).
  apply (TupleMap_direct_subterm_1_1 _ _ _ g).
Defined.

gives:

File "/home/greenrd/Documents/Bug.v", line 84, characters 0-8:
Error: Contexts do not agree for composition: x : nat; X1 : 
TupleT x; X2 : TupleT x; X0 : TupleMap x X1 X2; A : 
TupleT x; tm2 : TupleMap x A X1;
myComp : ∀ (n : nat) (i : sigT (λ _ : TupleT n, TupleT n))
     (y : TupleMap n (let (a, _) := i in a) (let (_, h) := i in h)),
     TupleMap_subterm
       (existT
      (λ i0 : {n0 : nat & sigT (λ _ : TupleT n0, TupleT n0)},
       TupleMap (let (a, _) := i0 in a)
         (let (a, _) :=
          let (x, h) as x
              return
            (sigT
               (λ _ : TupleT (let (a, _) := x in a),
                TupleT (let (a, _) := x in a))) := i0 in
          h in
          a)
         (let (_, h) :=
          let (x, h) as x
              return
            (sigT
               (λ _ : TupleT (let (a, _) := x in a),
                TupleT (let (a, _) := x in a))) := i0 in
          h in
          h))
      (existT (λ n0 : nat, sigT (λ _ : TupleT n0, TupleT n0)) n i) y)
       (existT
      (λ i0 : {n0 : nat & sigT (λ _ : TupleT n0, TupleT n0)},
       TupleMap (let (a, _) := i0 in a)
         (let (a, _) :=
          let (x, h) as x
              return
            (sigT
               (λ _ : TupleT (let (a, _) := x in a),
                TupleT (let (a, _) := x in a))) := i0 in
          h in
          a)
         (let (_, h) :=
          let (x, h) as x
              return
            (sigT
               (λ _ : TupleT (let (a, _) := x in a),
                TupleT (let (a, _) := x in a))) := i0 in
          h in
          h))
      (existT (λ n0 : nat, sigT (λ _ : TupleT n0, TupleT n0)) x
         (existT (λ _ : TupleT x, TupleT x) X1 X2)) X0)
     → (∀ A : TupleT n, TupleMap n A (projT1 i) → TupleMap n A (projT2 i))
|- x X1 X2 X0 A tm2 : x : nat; X1 : TupleT x; X2 : 
TupleT x; X0 : TupleMap x X1 X2; A : TupleT x;
tm2 : TupleMap x A X1 and n : nat; B : TupleT n; C : 
TupleT n; tm1 : TupleMap n B C; A : TupleT n; tm2 : 
TupleMap n A B |- n B C tm1 A tm2 : n : nat; B : TupleT n; C : 
TupleT n; tm1 : TupleMap n B C; A : TupleT n; tm2 : 
TupleMap n A B

Stackoverflow when using `rec (length l) lt`

I'm using OPAM-installed version of the Equations plugin (v1.0+8.7) with Coq v8.7.1.

The following code

From Equations Require Import Equations.

Equations silly {A} (l : list A) : list A :=
silly l by rec (length l) lt :=
silly nil := nil;
silly (cons a l) := a :: silly l.

generates

Error: Stack overflow.

If I remove the line with silly l by rec (length l) lt then it compiles:

Equations silly {A} (l : list A) : list A :=
silly nil := nil;
silly (cons a l) := a :: silly l.

Illegal application (Non-functional construction)

Another issue with another attempt at issue #78 workaround:

From Coq.Lists Require Import List.
From Equations Require Import Equations.

(* This type is from VST: https://github.com/PrincetonUniversity/VST/blob/v2.1/floyd/compact_prod_sum.v#L6 *)
Fixpoint compact_prod (T: list Type): Type :=
  match T with
  | nil => unit
  | t :: nil => t
  | t :: T0 => (t * compact_prod T0)%type
  end.

(* The rest is a nonsensical, just to give a minimalistic reproducible example *)
Inductive foo :=
| Nat : foo
| List : list foo -> foo.

Fixpoint foo_type (f:foo) : Type :=
  match f with
  | Nat => nat
  | List fs => compact_prod (map foo_type fs)
  end.

Equations num (f:foo) : forall (val:foo_type f), nat := {
  num Nat := fun val => val;
  num (List nil) := fun val => 0;
  num (List (cons hd tl)) := fun val => sum hd (num hd) tl val }
where (struct fs) sum (f:foo) (numf: (foo_type f -> nat)) (fs : list foo) (val: compact_prod (map foo_type (f::fs))) : nat := {
  sum f numf nil val := numf val;
  sum f numf (cons hd tl) val := numf (fst val) + sum hd (num hd) tl (snd val)}.

results in

Illegal application (Non-functional construction): 
The expression "f" of type "P Nat (fun val : foo_type Nat => val)"
cannot be applied to the terms
 "f3" : "foo"
 "numf" : "foo_type f3 -> nat"
 "[]" : "list foo"
 "val" : "compact_prod (map foo_type [f3])"
 "numf val" : "nat"

*_ind_fun cannot be proven

_ind_fun lemmas cannot be proven, because the defined function is by then "basically transparent but considered opaque for reduction", so it can't be unfolded.

Higher-order unification for Equations

Equations always says "Unable to split variable[...] to match a user pattern" if the argument to the function being defined refers to a function in the argument of a dependent type. This is because the unifier in equations gets stuck if it sees a function instead of a constructor.