Library ListFromRight.rl
Author: Jean-François Monin, Verimag, Université Grenoble Alpes
List traversal from right to left:
basic definitions to be used in foldl.v,
in particular an inductive domain for termination certificates,
with its projection and small inversions.
Contains improvements on material provided with D. Larchey-Wendling
in our chapter on the Braga Method (2021)
Require Import Utf8.
Require Import List.
Import ListNotations.
Reserved Notation "x '+:' y" (at level 59, left associativity, format "x +: y").
Fixpoint consr {A} (l : list A) (y : A) { struct l } : list A :=
match l with
| [] ⇒ [y]
| x :: l ⇒ x :: l +: y
end
where "x +: y" := (consr x y) : list_scope.
Inductive rl {A: Type} : list A → Type :=
| Nilr : rl []
| Consr : ∀ u z, rl (u +: z)
.
Section sec_context.
Context {A: Type}.
Implicit Type l u v : list A.
Implicit Type x y z : A.
Reflection function
Fixpoint l2r l : rl l :=
match l with
| [] ⇒ Nilr
| x :: v ⇒
match l2r v with
| Nilr ⇒ Consr [] x
| Consr u z ⇒ Consr (x :: u) z
end
end.
match l with
| [] ⇒ Nilr
| x :: v ⇒
match l2r v with
| Nilr ⇒ Consr [] x
| Consr u z ⇒ Consr (x :: u) z
end
end.
Basic but key lemma.
This is a proven equality, NOT a conversion.
Lemma l2r_consr : ∀ u z, l2r (u +: z) = Consr u z.
Proof.
intros u z; induction u as [ | x u Hu]; simpl.
- reflexivity.
- rewrite Hu. reflexivity.
Qed.
Proof.
intros u z; induction u as [ | x u Hu]; simpl.
- reflexivity.
- rewrite Hu. reflexivity.
Qed.
Inductively defined domain
𝔻listz u
---------- ----------------
𝔻listz [] 𝔻listz (u +: z)
Translated here as follows using rl, a dependent type:
𝔻listz u (l2r u)
--------------- ----------------------------
𝔻listz [] Nilr 𝔻listz (u +: z) (Consr u z)
Unset Elimination Schemes.
Inductive 𝔻listz : ∀ {l}, rl l → Prop :=
| 𝔻Nilr : 𝔻listz Nilr
| 𝔻Consr : ∀ u z, 𝔻listz (l2r u) → 𝔻listz (Consr u z)
.
Small inversion
Inductive is_𝔻Nilr : 𝔻listz Nilr → Prop :=
| is_𝔻Nilr_intro : is_𝔻Nilr 𝔻Nilr.
Inductive is_𝔻Consr u z : 𝔻listz (Consr u z) → Prop :=
| is_𝔻Consr_intro (d : 𝔻listz (l2r u)) : is_𝔻Consr u z (𝔻Consr u z d).
Definition 𝔻listz_inv {l} {r : rl l} (d : 𝔻listz r) :
match r with
| Nilr ⇒ is_𝔻Nilr
| Consr u z ⇒ is_𝔻Consr u z
end d.
Proof. destruct d; constructor. Defined.
| is_𝔻Nilr_intro : is_𝔻Nilr 𝔻Nilr.
Inductive is_𝔻Consr u z : 𝔻listz (Consr u z) → Prop :=
| is_𝔻Consr_intro (d : 𝔻listz (l2r u)) : is_𝔻Consr u z (𝔻Consr u z d).
Definition 𝔻listz_inv {l} {r : rl l} (d : 𝔻listz r) :
match r with
| Nilr ⇒ is_𝔻Nilr
| Consr u z ⇒ is_𝔻Consr u z
end d.
Proof. destruct d; constructor. Defined.
Structural projection
Definition π_𝔻listz_Consr {u} {z} (d: 𝔻listz (Consr u z)) : 𝔻listz (l2r u) :=
match d in 𝔻listz r return
let shape := match r with Consr u z ⇒ True | _ ⇒ False end in
let u := match r with Consr u z ⇒ u | _ ⇒ u end in
shape → 𝔻listz (l2r u) with
| 𝔻Consr u0 z0 D0 ⇒ λ _, D0
| _ ⇒ λ fa, match fa with end
end I.
Smaller inversion
Inductive is_𝔻Consr_π u z (d : 𝔻listz (Consr u z)) : 𝔻listz (Consr u z) → Prop :=
| is_𝔻Consr_π_intro: is_𝔻Consr_π u z d (𝔻Consr u z (π_𝔻listz_Consr d)).
Definition 𝔻listz_inv_π {l} {r : rl l} (d : 𝔻listz r) :
match r with
| Nilr ⇒ fun _ ⇒ is_𝔻Nilr
| Consr u z ⇒ is_𝔻Consr_π u z
end d d.
Proof. destruct d; constructor. Defined.
| is_𝔻Consr_π_intro: is_𝔻Consr_π u z d (𝔻Consr u z (π_𝔻listz_Consr d)).
Definition 𝔻listz_inv_π {l} {r : rl l} (d : 𝔻listz r) :
match r with
| Nilr ⇒ fun _ ⇒ is_𝔻Nilr
| Consr u z ⇒ is_𝔻Consr_π u z
end d d.
Proof. destruct d; constructor. Defined.
Dependent recursor (improvements on the Braga paper)
Definition 𝔻listz_rect (P: ∀ {l} (r : rl l), 𝔻listz r → Type) :
P Nilr 𝔻Nilr → (∀ u z d, P (l2r u) d → P (Consr u z) (𝔻Consr u z d)) →
∀ l (r: rl l) (d: 𝔻listz r), P r d.
Proof.
intros Pnil Pconsr.
refine (fix fxp l r d {struct d} : _ := _).
revert d.
destruct r as [| u z]; simpl; intros d.
- destruct (𝔻listz_inv_π d). apply Pnil.
- destruct (𝔻listz_inv_π d). apply Pconsr, fxp.
Defined.
The dependent induction principle can be seen as a corollary
of 𝔻listz_rect, but it has a simpler and direct proof on d
Definition 𝔻listz_ind (P: ∀ {l} (r: rl l), 𝔻listz r → Prop) :
P Nilr 𝔻Nilr → (∀ u z d, P (l2r u) d → P (Consr u z) (𝔻Consr u z d)) →
∀ l (r : rl l) (d: 𝔻listz r), P r d :=
fun PNilr PConsr ⇒
fix fxp l r d {struct d} : P r d :=
match d with
| 𝔻Nilr ⇒ PNilr
| 𝔻Consr u z d ⇒ PConsr u z d (fxp u (l2r u) d)
end.
Lemma 𝔻listz_all l : 𝔻listz (l2r l).
Proof.
induction l as [| x v d].
- exact 𝔻Nilr.
- induction d as [|u z d IHd].
+ exact (𝔻Consr [] x 𝔻Nilr).
+ change (x :: u +: z) with ((x :: u) +: z); rewrite l2r_consr.
apply (𝔻Consr (x :: u) z), IHd.
Qed.
End sec_context.
P Nilr 𝔻Nilr → (∀ u z d, P (l2r u) d → P (Consr u z) (𝔻Consr u z d)) →
∀ l (r : rl l) (d: 𝔻listz r), P r d :=
fun PNilr PConsr ⇒
fix fxp l r d {struct d} : P r d :=
match d with
| 𝔻Nilr ⇒ PNilr
| 𝔻Consr u z d ⇒ PConsr u z d (fxp u (l2r u) d)
end.
Lemma 𝔻listz_all l : 𝔻listz (l2r l).
Proof.
induction l as [| x v d].
- exact 𝔻Nilr.
- induction d as [|u z d IHd].
+ exact (𝔻Consr [] x 𝔻Nilr).
+ change (x :: u +: z) with ((x :: u) +: z); rewrite l2r_consr.
apply (𝔻Consr (x :: u) z), IHd.
Qed.
End sec_context.