James Wood (Sep 05 2022 at 12:33): James Wood (Sep 05 2022 at 12:33):My example uses Equations, but I think the real issue is with Coq's fix. I've been looking through Examples.RoseTree for inspiration on how to handle nested recursion. I was surprised that there, nested recursion seems to "just work" -- for example, size does not require inlining of list_size to satisfy termination checking. Even alt_size, which there is written in inlined style, can be rewritten in terms of map and list_max. However, when I try to write a size function on a more complex data structure -- intrinsically typed STLC with n-ary functions -- I get the error Cannot guess decreasing argument of fix. (see working example below). So, what termination heuristics are being hit by the rose tree example but not my STLC example, and is there any way that I could hit them?
Require Import List.
Import ListNotations.
From Equations Require Import Equations.
Inductive env {A} {T : A -> Type} : list A -> Type :=
| enil : env []
| econs {x xs} : T x -> env xs -> env (x :: xs).
Arguments env {A} T xs.
Equations env_map {A} {S T : A -> Type} :
(forall x, S x -> T x) ->
(forall xs, env S xs -> env T xs) :=
| f, _, enil => enil
| f, _, econs s ss => econs (f _ s) (env_map f _ ss).
Equations list_of_env {A T xs} : @env A (fun _ => T) xs -> list T :=
| enil => []
| econs t ts => t :: list_of_env ts.
Inductive type : Type :=
| base
| func (Ga : list type) (A : type).
Inductive elem {X} {x : X} : list X -> Type :=
| ze {xs} : elem (x :: xs)
| su {y xs} : elem xs -> elem (y :: xs).
Arguments elem {X} x xs.
Inductive term (Ga : list type) : type -> Type :=
| var {A} : elem A Ga -> term Ga A
| app {De A} : term Ga (func De A) -> env (term Ga) De -> term Ga A
| lam {De A} : term (De ++ Ga) A -> term Ga (func De A).
Arguments var {Ga A} & e.
Arguments app {Ga De A} M & Ns.
Arguments lam {Ga De A} M.
Fail Equations size {Ga A} : term Ga A -> nat :=
| var _ => 0
| app M Ns => S (size M + list_sum (list_of_env (env_map (fun _ => size) _ Ns)))
| lam M => S (size M)
.
Equations size {Ga A} : term Ga A -> nat := {
| var _ => 0
| app M Ns => S (size M + total_size Ns)
| lam M => S (size M)
}
where total_size {Ga De} : env (term Ga) De -> nat := {
| enil => 0
| econs t ts => size t + total_size ts
}
.
The trick in RoseTree is that in list_size the function f is introduced outside the Fixpoint.
Gaëtan Gilbert (Sep 05 2022 at 12:42):the problem is probably env_map recursing with too much generality
consider
Inductive rose := Node (_:list rose).
Fixpoint map1 {A B} (f:A->B) l :=
match l with
| nil => nil
| cons x l => cons (f x) (map1 f l)
end.
Definition map2 {A B} (f:A->B) :=
fix map2 l :=
match l with
| nil => nil
| cons x l => cons (f x) (map2 l)
end.
Axiom sum : list nat -> nat.
Fail Fixpoint size t :=
match t with
| Node l => sum (map1 size l)
end.
Fixpoint size t :=
match t with
| Node l => sum (map2 size l)
end.
map2 is the same as stdlib List.map
it can also be defined as
Section S.
Context {A B} (f:A->B).
Fixpoint map2 l :=
match l with
| nil => nil
| cons x l => cons (f x) (map2 l)
end.
so you can try defining env_map in sections with the arguments that are constant in the recursion pulled out as section variables to get equations to do the right thing.
James Wood (Sep 05 2022 at 12:46):Aha, indeed, defining env_map in a section fixed it!
James Wood (Sep 05 2022 at 12:49):So is the later fix doing some analysis of map1/map2/env_map that gets caught up when that earlier fix-expression is too complicated?
Gaëtan Gilbert (Sep 05 2022 at 12:54):it does some reduction ending up with seeing
(fix map1 A B f l := ...) _ _ size l
vs
(fix map2 l := ... size ...) l
the information that l is a subterm of t is propagated through the fixes in both cases, but in the first case it still sees a not applied size so rejects it
Notification Bot (Sep 05 2022 at 12:56):James Wood has marked this topic as resolved.
Last updated: Oct 05 2023 at 02:01 UTC