Require Export Bool Omega List PrelimsTac Compat.Coq86 (* for Functional Induction*).
Global Set Implicit Arguments.
Global Unset Strict Implicit.
Global Set Warnings "-notation-overridden,-parsing".
Export ListNotations.
Global Set Implicit Arguments.
Global Unset Strict Implicit.
Global Set Warnings "-notation-overridden,-parsing".
Export ListNotations.
Preliminaries
Definition dec (X: Prop) : Type := {X} + {~ X}.
Existing Class dec.
Definition Dec (X: Prop) (d: dec X) : dec X := d.
Arguments Dec X {d}.
Tactic Notation "decide" constr(p) :=
destruct (Dec p).
Tactic Notation "decide" "_" :=
destruct (Dec _).
Existing Class dec.
Definition Dec (X: Prop) (d: dec X) : dec X := d.
Arguments Dec X {d}.
Tactic Notation "decide" constr(p) :=
destruct (Dec p).
Tactic Notation "decide" "_" :=
destruct (Dec _).
Lemma size_induction X (f : X -> nat) (p : X -> Prop) :
(forall x, (forall y, f y < f x -> p y) -> p x) ->
forall x, p x.
Proof.
intros IH x. apply IH.
assert (G: forall n y, f y < n -> p y).
{ intros n. induction n.
- intros y B. exfalso. omega.
- intros y B. apply IH. intros z C. apply IHn. omega. }
apply G.
Qed.
Instance nat_le_dec (x y : nat) : dec (x <= y) :=
le_dec x y.
Notation "'eq_dec' X" := (forall x y : X, dec (x=y)) (at level 70).
Instance nat_eq_dec :
eq_dec nat.
Proof.
unfold dec. decide equality.
Defined.
Notation "| A |" := (length A) (at level 65).
(*Notation for lookup*)
Notation "A .[ n ]" := (nth_error A n) (at level 1, format "A '.[' n ]").
Notation "x '∈' A" := (In x A) (at level 70).
(* some lemmas not included in the standard library: *)
Lemma nth_error_lt_Some A (H:list A) n : n < |H| -> exists x, H.[n] = Some x.
Proof.
intros eq. revert H eq. induction n;intros;destruct H;cbn in *;inv eq;eauto. all:edestruct (IHn H); try omega; eauto.
Qed.
Lemma nth_error_Some_lt A (H:list A) n x : H.[n] = Some x -> n < |H|.
Proof.
intros eq. revert H eq. induction n;intros;destruct H;cbn in *;inv eq. omega. apply IHn in H1. omega.
Qed.
Lemma nth_error_map A B (H:list A) (f:A->B) n a : (map f H).[n] = Some a -> exists b, H.[n] = Some b /\ a = f b.
Proof.
intros eq. revert H eq. induction n;intros;destruct H;cbn in *;inv eq. eauto. eauto.
Qed.
Lemma Forall_map X Y (A:list X) p (f:X->Y):
Forall (fun x => p (f x)) A -> Forall p (map f A).
Proof.
rewrite !Forall_forall. setoid_rewrite in_map_iff. firstorder subst. eauto.
Qed.
Hint Extern 4 =>
match goal with
|[ H: ?x ∈ nil |- _ ] => destruct H
end.
(* Register additional simplification rules with autorewrite*)
Hint Rewrite <- app_assoc : list.
(*Notation for lookup*)
Notation "A .[ n ]" := (nth_error A n) (at level 1, format "A '.[' n ]").
Notation "x '∈' A" := (In x A) (at level 70).
(* some lemmas not included in the standard library: *)
Lemma nth_error_lt_Some A (H:list A) n : n < |H| -> exists x, H.[n] = Some x.
Proof.
intros eq. revert H eq. induction n;intros;destruct H;cbn in *;inv eq;eauto. all:edestruct (IHn H); try omega; eauto.
Qed.
Lemma nth_error_Some_lt A (H:list A) n x : H.[n] = Some x -> n < |H|.
Proof.
intros eq. revert H eq. induction n;intros;destruct H;cbn in *;inv eq. omega. apply IHn in H1. omega.
Qed.
Lemma nth_error_map A B (H:list A) (f:A->B) n a : (map f H).[n] = Some a -> exists b, H.[n] = Some b /\ a = f b.
Proof.
intros eq. revert H eq. induction n;intros;destruct H;cbn in *;inv eq. eauto. eauto.
Qed.
Lemma Forall_map X Y (A:list X) p (f:X->Y):
Forall (fun x => p (f x)) A -> Forall p (map f A).
Proof.
rewrite !Forall_forall. setoid_rewrite in_map_iff. firstorder subst. eauto.
Qed.
Hint Extern 4 =>
match goal with
|[ H: ?x ∈ nil |- _ ] => destruct H
end.
(* Register additional simplification rules with autorewrite*)
Hint Rewrite <- app_assoc : list.
Definition rcomp X Y Z (R : X -> Y -> Prop) (S : Y -> Z -> Prop) : X -> Z -> Prop :=
fun x z => exists y, R x y /\ S y z.
Structure ARS :=
{
ARS_X :> Type ;
ARS_R : ARS_X -> ARS_X -> Prop
}.
Notation "(≻)" := (@ARS_R _) (at level 0).
Notation "(≻ X )" := (@ARS_R X) (at level 0).
Notation "x ≻ x'" := (ARS_R x x') (at level 40).
Definition reducible (X : Type) (R : X -> X -> Prop) x :=
exists x', R x x'.
Hint Unfold reducible.
Definition functional (X Y : Type) (R : X -> Y -> Prop) :=
forall x y y', R x y -> R x y' -> y = y'.
Definition stepFunction {X Y} (R: X -> Y -> Prop) f :=
forall x, match f x with
Some y => R x y
| None => forall y, ~ R x y
end.
Definition computable {X Y} (R:X -> Y -> Prop) :=
exists f, stepFunction R f.
Definition classical {X} R := forall s : X, reducible R s \/ ~ reducible R s.
Lemma computable_classical X (R:X -> X -> Prop):
computable R -> classical R.
Proof.
intros [f C] x. specialize (C x). destruct (f x). now left; eauto. right;intros [? ?]. eapply C. eauto.
Qed.
(* missing facts about relation extension on lists *)
Lemma Forall2_impl X Y (P1 P2:X->Y->Prop) A B: (forall x y, P1 x y -> P2 x y) -> Forall2 P1 A B -> Forall2 P2 A B.
Proof.
intros ? H. induction H;cbn in *;eauto.
Qed.
Inductive terminatesOn (X : Type) (R : X -> X -> Prop) x: Prop :=
terminatesC (wf: forall x', R x x' -> terminatesOn R x').
Reserved Notation "x ▷ z" (at level 40).
Inductive evaluates (X : ARS) : X -> X -> Prop :=
evaluates_B (x : X) : ~ reducible (≻) x -> x ▷ x
| evaluates_S (x y z : X) : x ≻ y -> y ▷ z -> x ▷ z
where "x ▷ z" := (@evaluates _ x z).
Notation "(▷)" := (@evaluates _) (at level 0).
Notation "(▷ X )" := (@evaluates X) (at level 0).
(* workaround to prefere "x ≻ y" over "(≻) x y"*) Notation "x ▷ x'" := 0.
Notation "x ▷ x'" := (@evaluates _ x x').
Definition normalizes (X : ARS) (x:X) :=
exists y, x ▷ y.
Hint Unfold normalizes.
Lemma evaluates_fun (X : ARS) :
functional (≻X) -> functional (▷X).
Proof.
intros FN x x' x'' H. revert x''. induction H.
- intros. inv H0.
+ reflexivity.
+ destruct H; eauto.
- intros. inv H1.
+ destruct H2; eauto.
+ eapply IHevaluates. now rewrite (FN _ _ _ H H2).
Qed.
Lemma normalizes_terminates (X : ARS) :
functional (≻X) ->
forall (x:X), normalizes x -> terminatesOn (≻) x.
Proof.
intros FN x [x' ?]. induction H.
- econstructor. intros x' ?; destruct H. eauto.
- econstructor. intros x' ?. now rewrite (FN _ _ _ H1 H).
Qed.
Lemma terminates_normalizes (X : ARS) :
computable (≻X) ->
forall (x:X), terminatesOn (≻) x -> normalizes x.
Proof.
intros C%computable_classical x. induction 1.
destruct (C x) as [ [a' Hstep] | ].
- destruct (H _ Hstep) as [a'']. exists a''. eauto using evaluates.
- exists x. now econstructor.
Qed.
Lemma evaluates_irred (X : ARS) (x y : X):
x ▷ y -> ~ reducible (≻) y.
Proof.
induction 1; eauto.
Qed.
Fixpoint noneHolds (Ps :list Prop) : Prop :=
match Ps with
| [] => True
| P :: Ps => ~ P /\ noneHolds Ps
end.
Fixpoint exactlyOneHolds (Ps :list Prop) : Prop :=
match Ps with
| [] => False
| P :: Ps => P /\ noneHolds Ps \/ ~ P /\ exactlyOneHolds Ps
end.
Ltac noneHoldsI :=
lazymatch goal with
|- noneHolds [] => now constructor
| |- noneHolds (_::_) => split;[|noneHoldsI]
end.
Ltac exactlyOneHoldsI n :=
lazymatch n with
| 1 => left;split;[|noneHoldsI]
| S ?n => right;split;[|exactlyOneHoldsI n]
end.
Ltac inv_noneHolds H :=
lazymatch type of H with
| noneHolds [] => clear H
| noneHolds (_::_) => let tmp := fresh "tmp" in destruct H as [? tmp];inv_noneHolds tmp
end.
Ltac inv_exactlyOneHolds H :=
lazymatch type of H with
| exactlyOneHolds [] => now inversion H
| exactlyOneHolds (_::_) => let tmp := fresh "tmp" in destruct H as [[? tmp]|[? tmp]];[inv_noneHolds tmp|inv_exactlyOneHolds tmp]
end.
Nicer Notation for Option