Library Coq.Wellfounded.Lexicographic_Exponentiation
Author: Cristina Cornes
From : Constructing Recursion Operators in Type Theory
L. Paulson JSC (1986) 2, 325-355
Require Import List.
Require Import Relation_Operators.
Require Import Transitive_Closure.
Section Wf_Lexicographic_Exponentiation.
Variable A :
Set.
Variable leA :
A ->
A ->
Prop.
Notation Power := (
Pow A leA).
Notation Lex_Exp := (
lex_exp A leA).
Notation ltl := (
Ltl A leA).
Notation Descl := (
Desc A leA).
Notation List := (
list A).
Notation Nil := (
nil (
A:=
A)).
Notation Cons := (
cons (
A:=
A)).
Notation "<< x , y >>" := (
exist Descl x y) (
at level 0,
x,
y at level 100).
Lemma left_prefix :
forall x y z:
List,
ltl (
x ++ y)
z ->
ltl x z.
Lemma right_prefix :
forall x y z:
List,
ltl x (
y ++ z) ->
ltl x y \/ (exists y' : List, x = y ++ y' /\ ltl y' z).
Lemma desc_prefix :
forall (
x:
List) (
a:
A),
Descl (
x ++ Cons a Nil) ->
Descl x.
Lemma desc_tail :
forall (
x:
List) (
a b:
A),
Descl (
Cons b (
x ++ Cons a Nil)) ->
clos_trans A leA a b.
Lemma dist_aux :
forall z:
List,
Descl z ->
forall x y:
List,
z = x ++ y ->
Descl x /\ Descl y.
Lemma dist_Desc_concat :
forall x y:
List,
Descl (
x ++ y) ->
Descl x /\ Descl y.
Lemma desc_end :
forall (
a b:
A) (
x:
List),
Descl (
x ++ Cons a Nil)
/\ ltl (
x ++ Cons a Nil) (
Cons b Nil) ->
clos_trans A leA a b.
Lemma ltl_unit :
forall (
x:
List) (
a b:
A),
Descl (
x ++ Cons a Nil) ->
ltl (
x ++ Cons a Nil) (
Cons b Nil) ->
ltl x (
Cons b Nil).
Lemma acc_app :
forall (
x1 x2:
List) (
y1:
Descl (
x1 ++ x2)),
Acc Lex_Exp << x1 ++ x2, y1 >> ->
forall (
x:
List) (
y:
Descl x),
ltl x (
x1 ++ x2) ->
Acc Lex_Exp << x, y >>.
Theorem wf_lex_exp :
well_founded leA ->
well_founded Lex_Exp.
End Wf_Lexicographic_Exponentiation.