How to formalize the ending of a term abbreviation relationship in Coq?
I have a term rewriting system (A, →) where A is a set and → a binary infix relation on A. For x and y from A, x → y means x is reduced to y.
To implement some properties, I just use definitions from Coq.Relations.Relation_Definitions
and Coq.Relations.Relation_Operators
.
Now I want to formalize the following property:
- → ends, that is: there is no infinite descending chain a0 → a1 → ...
How can I achieve this in Coq?
source to share
Showing that the rewrite relationship is complete is the same as showing that it is valid. This can be coded by an inductive predicate in Coq:
Inductive Acc {A} (R : A -> A -> Prop) (x: A) : Prop :=
Acc_intro : (forall y:A, R x y -> Acc R y) -> Acc R x.
Definition well_founded {A} (R : A -> A -> Prop) :=
forall a:A, Acc R a.
(This definition is essentially one of the predicates Acc
, and well_founded
the standard library, but I have changed the order of the ratio to match the conventions used in rewriting systems.)
Given the type A
and relation R
to A
, Acc R x
means that each sequence of abbreviations R
, starting with x : A
, ends; thus well_founded R
means that every sequence starting at any point ends. ( Acc
means "available".)
It is perhaps not entirely clear why this definition works; First, how can we show what Acc R x
is true for anyone x
at all? Note that if x
- the element does not decrease (ie one that R x y
never holds for anyone y
), then the premise Acc_intro
is trivially satisfied, and we can conclude Acc R x
. For example, this would allow us to show Acc gt 0
. If R
indeed justified, we can work backwards from such base cases and conclude that other elements are available A
. A formal proof of validity is more complex than this because it should work in general for everyone x
, but it at least shows how we could show that each item is available separately.
OK, so maybe we can show what's going on Acc R x
. How do we use it? With the principles of induction and recursion that Coq generates for Acc
; eg:
Acc_ind : forall A (R : A -> A -> Prop) (P : A -> Prop),
(forall x : A, (forall y : A, R x y -> P y) -> P x) ->
forall x : A, Acc R x -> P x
When R
justified, it is simply the principle of justified induction. We can rephrase it as follows. Suppose we can show what P x
holds for anyone x : A
by using the induction hypothesis, which says what P y
holds whenever R x y
. (Depending on the value, R
this can mean that it x
takes steps y
or that it is y
strictly less than x
, etc.). Then it P x
holds for any x
such that Acc R x
. Well-founded recursion works in a similar way and intuitively expresses that the recursive definition is true if each recursive call is made on "smaller" elements.
Adam Chlipala CPDT has a chapter on general recursion that has a fuller coverage of this stuff.
source to share