Library hydras.solutions_exercises.MultisetWf
Set Implicit Arguments.
Require Import Relations List Sorted Arith.
From hydras Require Import Restriction.
From Coq Require Import Lia.
Definition t (A:Type) := list (A × nat).
Section A_given.
Variable A: Type.
Variable LtA : relation A.
Inductive lexpower: relation (t A) :=
lex1: ∀ a n l, lexpower nil ((a,n)::l)
| lex2: ∀ a n p l l', n < p → lexpower ((a,n)::l) ((a,p)::l')
| lex3: ∀ a b n p l l', LtA a b → lexpower ((a,n)::l) ((b,p)::l')
| lex4: ∀ a n l l', lexpower l l' → lexpower ((a,n)::l) ((a,n)::l').
End A_given.
Section Counter_Example.
Let R := lexpower lt.
Hypothesis Hwf : well_founded R.
Definition seq (n:nat) := repeat (0,0) n ++ ((2,0)::nil).
Lemma decr_seq : ∀ n, R (seq (S n)) (seq n).
Lemma not_acc : ∀ a b, R a b → ¬ Acc R a → ¬ Acc R b.
Let is_in_seq l := ∃ i, l = seq i.
Lemma is_in_seq_not_Acc : ∀ x, is_in_seq x → ¬ Acc R x.
Lemma contrad: False.
End Counter_Example.
Require Import Relations List Sorted Arith.
From hydras Require Import Restriction.
From Coq Require Import Lia.
Definition t (A:Type) := list (A × nat).
Section A_given.
Variable A: Type.
Variable LtA : relation A.
Inductive lexpower: relation (t A) :=
lex1: ∀ a n l, lexpower nil ((a,n)::l)
| lex2: ∀ a n p l l', n < p → lexpower ((a,n)::l) ((a,p)::l')
| lex3: ∀ a b n p l l', LtA a b → lexpower ((a,n)::l) ((b,p)::l')
| lex4: ∀ a n l l', lexpower l l' → lexpower ((a,n)::l) ((a,n)::l').
End A_given.
Section Counter_Example.
Let R := lexpower lt.
Hypothesis Hwf : well_founded R.
Definition seq (n:nat) := repeat (0,0) n ++ ((2,0)::nil).
Lemma decr_seq : ∀ n, R (seq (S n)) (seq n).
Lemma not_acc : ∀ a b, R a b → ¬ Acc R a → ¬ Acc R b.
Let is_in_seq l := ∃ i, l = seq i.
Lemma is_in_seq_not_Acc : ∀ x, is_in_seq x → ¬ Acc R x.
Lemma contrad: False.
End Counter_Example.
Lists in normal form
Definition lexnf {A: Type}(ltA : relation A) (l: t A)
:= LocallySorted (Basics.flip ltA) (map fst l).
Definition lexlt {A}(ltA : relation A) :=
restrict (lexnf ltA) (lexpower ltA).
Section ProofOfLexwf.
Variables (A: Type)
(ltA : relation A).
Hypothesis HwfA : well_founded ltA.
#[local] Notation NF := (lexnf ltA).
#[local] Notation LT := (lexlt ltA).
Theorem lexwf:
∀ l, NF l → Acc LT l.
Lemma NF_inv1 : ∀ a n l, NF ((a,n)::l) → NF l.
Lemma NF_inv2 : ∀ a n b p l, NF((a,n)::(b,p)::l) → ltA b a.
Lemma LT_inv : ∀ a n l l',
LT l' ((a,n)::l) →
l' = nil ∨
(∃ b p l'', l'= ((b,p)::l'') ∧ ltA b a) ∨
(∃ l'', l'=(a,n)::l'' ∧ LT l'' l) ∨
(∃ p l'', l'= ((a,p)::l'') ∧ p < n).
Let Accs (a:A) := ∀ n l, NF ((a,n)::l) →
Acc LT ((a,n)::l).
Lemma Acc_nil : Acc LT nil.
Lemma Accs_all: ∀ a:A, Accs a.
let us prepare an induction on l
Lemma NF_Acc : ∀ l: t A, NF l → Acc LT l.
End ProofOfLexwf.
Theorem lexwf {A}( ltA : relation A) :
well_founded ltA →
∀ l, lexnf ltA l → Acc (lexlt ltA) l.
Example Ex1 : lexpower lt ((2,7)::nil) ((3,0):: nil).
Example Ex2 : lexpower lt ((2,7)::(1,0)::(0,33)::nil) ((2,7)::(1,6)::nil).
Example Ex3 : lexnf lt ((2,7)::(1,0)::(0,33)::nil).
Section Impossibility1.
Variable m : t nat → nat.
Hypothesis mDecr : ∀ l l': t nat, lexlt lt l l' → m l < m l'.
Definition iota (n:nat) := (0, n)::nil.
Let x := m ((1,0)::nil).
Let y := m (iota x).
Fact F1 : y < x.
Fact F2 : x ≤ y.
Lemma impossible_nat : False.
End Impossibility1.