Created
April 28, 2014 15:12
-
-
Save aspiwack/11375022 to your computer and use it in GitHub Desktop.
The impredicative encoding of list has associativity of concatenation up to conversion! (requires -impredicative-set)
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(* -*- coq-prog-args: ("-emacs-U" "-impredicative-set") -*- *) | |
Require Coq.Lists.List. | |
Definition IList (A:Set) : Set := | |
forall R:Set, (A->R->R) -> R -> R | |
. | |
Definition empty {A:Set} : IList A := | |
fun R c e => e | |
. | |
Arguments empty {A} R c e /. | |
Definition single {A:Set} (x:A) : IList A := | |
fun R c e => c x e | |
. | |
Arguments single {A} x R c e /. | |
Definition app {A:Set} (l r:IList A) : IList A := | |
fun R c e => l R c (r R c e) | |
. | |
Arguments app {A} l r R c e /. | |
Notation "l ++ r" := (app l r). | |
Definition cons {A:Set} (x:A) (l:IList A) : IList A := (single x)++l. | |
Arguments cons {A} x l R c e /. | |
Remark app_empty_neutral_r : forall A (l:IList A), l++empty = l. | |
Proof. | |
intros **. | |
reflexivity. | |
Qed. | |
Remark app_empty_neutral_l : forall A (l:IList A), empty++l = l. | |
Proof. | |
intros **. | |
reflexivity. | |
Qed. | |
Remark app_associative : forall A (l r q:IList A), (l++r)++q = l++(r++q). | |
Proof. | |
intros **. | |
reflexivity. | |
Qed. | |
Definition fold_right {A B:Set} (f:A->B->B) (s:B) (l:IList A) : B := l B f s. | |
Definition ilist_rec0 {A B:Set} (s:B) (f:A->IList A->B->B) (l:IList A) : B := | |
snd (fold_right (fun a lb => (cons a (fst lb) , f a (fst lb) (snd lb))) (empty,s) l) | |
. | |
(** Parametricity and is needed to show that impredicative lists are equivalent to lists *) | |
Notation "A ⇔ B" := (A->B->Prop) (at level 70). | |
Definition arrow_rel {A A' B B':Type} (rA:A⇔A') (rB:B⇔B') : (A->B)⇔(A'->B') := | |
fun f g => forall x y, rA x y -> rB (f x) (g y) | |
. | |
Arguments arrow_rel {A A' B B'} rA rB f g /. | |
Notation "rA ⟶ rB" := (arrow_rel rA rB) (at level 70, right associativity). | |
Definition forall_rel {B₁:Set->Set} {B₂:Set->Set} | |
(rB:forall (A₁ A₂:Set) (r:A₁⇔A₂), B₁ A₁⇔B₂ A₂) : (forall x, B₁ x) ⇔ (forall x, B₂ x) := | |
fun f g => forall (A₁ A₂:Set) (rA:A₁⇔A₂), rB A₁ A₂ rA (f A₁) (g A₂) | |
. | |
Notation "∀ ( r : A₁ ⇔ A₂ ) , rB" := (forall_rel (fun A₁ A₂ r => rB)) (at level 90, r ident, A₁ ident, A₂ ident). | |
Definition Parametric {A:Set} (rA:A⇔A) (l:IList A) : Prop := | |
(∀ (r:R⇔R'), (rA ⟶ r ⟶ r) ⟶ r ⟶ r) l l | |
. | |
Definition list_to_ilist {A:Set} (l:list A) : IList A := | |
List.fold_right cons empty l | |
. | |
Definition ilist_to_list {A:Set} (l:IList A) : list A := | |
fold_right (@List.cons _) List.nil l | |
. | |
Lemma list_retract : forall (A:Set) (l:list A), ilist_to_list (list_to_ilist l) = l. | |
Proof. | |
intros A l. | |
induction l as [|x l h]. | |
+ easy. | |
+ simpl. unfold cons,single,app,ilist_to_list,fold_right in *. | |
congruence. | |
Qed. | |
(* Basic usage of parametricity, as an example *) | |
Remark ilist_param_cons_empty_id : forall (A:Set) (l:IList A), Parametric (@eq A) l -> | |
forall R c e, l _ cons empty R c e = l R c e. | |
Proof. | |
intros * param *. | |
specialize (param (IList A) R (fun l z => l R c e = z)). simpl in param. | |
apply param. | |
+ intros x y <- l' z' h. | |
simpl. | |
congruence. | |
+ easy. | |
Qed. | |
Lemma ilist_param_retract : forall (A:Set) (l:IList A), Parametric (@eq A) l -> | |
forall R c e, list_to_ilist (ilist_to_list l) R c e = l R c e. | |
Proof. | |
intros * param *. | |
unfold ilist_to_list,fold_right. | |
specialize (param (list A) R (fun l z => list_to_ilist l R c e = z)). simpl in param. | |
apply param. | |
+ intros x y <- l' z' h. | |
simpl. | |
congruence. | |
+ easy. | |
Qed. | |
(** Induction is harder than recursion because it is not true without | |
parametricity or functional extensionality. Apart from that, it is | |
basically the same definition as [ilist_rec0], but with [{l:IList | |
A|P x}] instead of [(IList A*B)]. *) | |
Theorem ilist_param_ind (A:Set) (P:IList A->Prop) | |
(s:P empty) (f:forall (x:A) (l:IList A), P l -> P (cons x l)) (l:IList A) : | |
Parametric (@eq A) l -> (forall l', (forall R c e, l' R c e = l R c e) -> l'=l) -> P l. | |
Proof. | |
intros param ext. | |
set (ind:= fold_right | |
(fun a lp => exist P (cons a (proj1_sig lp)) (f a (proj1_sig lp) (proj2_sig lp))) | |
(exist P empty s) | |
l). | |
assert (proj1_sig ind = l) as h. | |
{ apply ext. intros R c e. | |
unfold ind, fold_right. | |
specialize (param {x|P x} R (fun lp z => proj1_sig lp R c e = z)). simpl in param. | |
apply param. | |
+ intros x y <- lp z h. | |
simpl. | |
now rewrite <- h. | |
+ easy. } | |
rewrite <- h. | |
exact (proj2_sig ind). | |
Qed. | |
(** Assuming that every [IList A] is parametric together with | |
functional extensionality allow to recover the convenience of | |
usual lists with the exception of fixed points. *) | |
Require Import Coq.Logic.FunctionalExtensionality. | |
Axiom ilist_param : forall (A:Set) (r:A⇔A) (l:IList A), Parametric r l. | |
Corollary ilist_ind (A:Set) (P:IList A->Prop) | |
(s:P empty) (f:forall (x:A) (l:IList A), P l -> P (cons x l)) (l:IList A) : P l. | |
Proof. | |
intros **. | |
apply ilist_param_ind; try solve[easy|apply ilist_param]. | |
intros **. | |
extensionality R; extensionality c; extensionality e. | |
easy. | |
Qed. | |
Lemma fold_right_empty (A B:Set) (f:A->B->B) (s:B) : fold_right f s empty = s. | |
Proof. reflexivity. Qed. | |
Lemma fold_right_cons (A B:Set) (f:A->B->B) (s:B) x l : | |
fold_right f s (cons x l) = f x (fold_right f s l). | |
Proof. reflexivity. Qed. | |
Theorem ilist_rec0_empty (A B:Set) (s:B) (f:A->IList A -> B -> B) : ilist_rec0 s f empty = s. | |
Proof. reflexivity. Qed. | |
(** Contrary to the case true inductive type, this property needs to | |
be proven by induction. *) | |
Theorem ilist_rec0_cons (A B:Set) (s:B) (f:A->IList A -> B -> B) x l : | |
ilist_rec0 s f (cons x l) = f x l (ilist_rec0 s f l). | |
Proof. | |
unfold ilist_rec0. | |
simpl. | |
f_equal. clear. | |
induction l as [ | x l h ] using ilist_ind. | |
+ easy. | |
+ simpl. | |
congruence. | |
Qed. | |
Remark conj_injective (A:Set) (x₁ x₂:A) (l₁ l₂:IList A) : | |
cons x₁ l₁ = cons x₂ l₂ -> x₁ = x₂ /\ l₁ = l₂. | |
Proof. | |
intros h. | |
split. | |
+ apply | |
(f_equal (ilist_rec0 x₁(*this x₁ is not used, it just fills the gap*) (fun a _ _ => a)) h). | |
+ (* The list case is harder because it does not reduce up to conversion. *) | |
set (tl := (ilist_rec0 l₁ (fun _ l _ => l))). | |
assert (forall l x, tl (cons x l) = l) as def. | |
{ clear. subst tl. intros **. | |
rewrite ilist_rec0_cons. | |
reflexivity. } | |
rewrite <- (def l₁ x₁) , <- (def l₂ x₂). | |
congruence. | |
Qed. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment