mattam82 / coq-equations Goto Github PK
View Code? Open in Web Editor NEWA function definition package for Coq
Home Page: http://mattam82.github.io/Coq-Equations
License: GNU Lesser General Public License v2.1
A function definition package for Coq
Home Page: http://mattam82.github.io/Coq-Equations
License: GNU Lesser General Public License v2.1
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
.
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
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
}.
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.)
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").
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.
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.
After a short discussion with @mattam82 , it seems that it might be possible to build noCycle using well-foundedness of Subterm.
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?
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.
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 *)
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".
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.
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.
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".
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.
Running coq_makefile -f _CoqProject -o Makefile
produces:
Warning: -extra and -extra-phony are deprecated.
Warning: Write the extra targets in Makefile.local.
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"
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 *)
As mentioned in issue 8.
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
.
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.
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.
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. *)
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.
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 =============================#
=-=- 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
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.
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.
The source file equations.ml fails to compile due to changes in the API of the Constrintern module.
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.
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.
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.
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.
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?
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.
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
Currently it gives 87 on the 8.8+alpha branch!
_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.
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.
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.
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...
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
).
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
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.
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?
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.
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
.
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
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))}.
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?
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.