Commit 743686f0 authored by charguer's avatar charguer

progress

parent 52584dfc
(* DEPRECATEd: int_nat_plus_abs => *)
(* DEPRECATED: see plus_nat_int
Lemma int_nat_plus : forall (x y:nat),
my_Z_of_nat (x + y)%nat = (my_Z_of_nat x + my_Z_of_nat y).
Proof using. math. Qed.
*)
(* DEPRECATED => lt_nat_of_lt_int
Lemma int_nat_lt : forall (x y:nat),
((x:int) < (y:int)) -> x < y.
Proof using. math. Qed.
*)
(* DEPRECATED => eq_int_of_eq_nat
Lemma nat_int_eq : forall (x y:nat),
(x = y :> nat) -> (x = y :> int).
Proof using. math. Qed.
*)
(* DEPRECATED update_map => map_update *)
......@@ -21,10 +21,6 @@ Generalizable Variables A B.
Require Import LibNat LibInt.
Lemma int_nat_lt : forall (x y:nat),
((x:int) < (y:int)) -> x < y.
Proof using. math. Qed.
Section NatSimpl.
Open Scope nat_scope.
Implicit Types n : nat.
......@@ -63,257 +59,18 @@ Hint Rewrite nat_zero_plus nat_plus_zero nat_plus_succ
nat_minus_zero nat_succ_minus_succ
nat_minus_same nat_plus_minus_same : rew_nat.
(* Already exists
Tactic Notation "rew_nat" :=
autorewrite with rew_nat.
Tactic Notation "rew_nat" "in" "*" :=
autorewrite with rew_nat in *.
Tactic Notation "rew_nat" "in" hyp(H) :=
autorewrite with rew_nat in H.
*)
Lemma int_nat_plus : forall (x y:nat),
my_Z_of_nat (x + y)%nat = (my_Z_of_nat x + my_Z_of_nat y).
Proof using. math. Qed.
Lemma int_nat_plus_abs : forall k n,
n >= 0 ->
(k + abs n)%nat = abs (k + n)%Z.
Proof using.
introv N. applys eq_int_nat.
rewrite int_nat_plus.
do 2 (rewrite abs_pos; [|math]).
auto.
Qed.
Lemma nat_int_eq : forall (x y:nat),
(x = y :> nat) -> (x = y :> int).
Proof using. math. Qed.
(*----------------------*)
(* List *)
Require Import LibList.
Open Scope list_scope.
Lemma list_middle_inv : forall A (n:nat) (L:list A),
(0 <= n < length L)%nat ->
exists L1 x L2, L = L1++x::L2 /\ length L1 = n.
Proof using.
intros. gen L. induction n; introv N;
destruct L as [|x L']; rew_list in *; try solve [ false; math ].
{ exists~ (@nil A) x L'. }
{ forwards (L1&x'&L2&E&M): IHn L'. math.
exists (x::L1) x' L2. subst L'. rew_list~. }
Qed.
Lemma nth_map : forall `{IA:Inhab A} `{IB:Inhab B} (l:list A) (i:nat) (f:A->B),
i < length l ->
nth i (map f l) = f (nth i l).
Proof using.
introv I. gen i. induction l; intros; rew_list in *.
{ false; math. }
{ destruct i as [|i'].
{ do 2 rewrite nth_zero. auto. }
{ do 2 rewrite nth_succ. applys IHl. math. } }
Qed.
Lemma list_update_map : forall A B (l:list A) (i:nat) (x:A) (f:A->B),
i < length l ->
map f (LibList.update i x l) = LibList.update i (f x) (map f l).
Proof using.
introv I. gen i. induction l; intros; rew_list in *.
{ false; math. }
{ destruct i as [|i']; simpl update; rew_map.
{ auto. }
{ fequals. applys IHl. math. } }
Qed.
Section Combine.
Variable (A B : Type).
Implicit Types r : list A.
Implicit Types s : list B.
Lemma combine_cons : forall x r y s,
combine (x::r) (y::s) = (x,y)::(combine r s).
Proof using. auto. Qed.
End Combine.
(*----------------------*)
(* ListZ *)
Require Import LibLogic.
Require LibListZ.
Module ReadProperties.
Import LibListZ.
Transparent index_inst read_inst update_inst.
Lemma read_middle : forall A `{IA:Inhab A} i (L1 L2 : list A) x,
i = length L1 ->
(L1 ++ x :: L2)[i] = x.
Proof.
intros.
unfold LibBag.read, read_inst, read_impl.
unfold nth. case_if. { false; math. }
(* TODO: use new TLC lemmas about nth *)
applys LibList.Nth_to_nth. applys Nth_app_r 0%nat.
constructors. applys eq_int_nat. rewrite abs_pos; math.
Qed.
Lemma Nth_nth_if_in_length:
forall A `{IA:Inhab A} (l : list A) (n : nat),
n < LibList.length l -> Nth n l (LibList.nth n l).
Proof using.
intros. applys* nth_def_if_in_length.
Qed.
Lemma nth_app_l : forall k A (d:A) (L1 L2:list A),
(k < LibList.length L1)%nat ->
nth_def d k (L1 ++ L2) = nth_def d k L1.
Proof using.
intros k; induction k; introv N.
{ destruct L1 as [|x L1'].
{ rew_list in *. false. math. }
{ rew_list in *. auto. } }
{ destruct L1 as [|x L1'].
{ rew_list in *. false. math. }
{ rew_list in *. simpl. applys IHk. math. } }
Qed.
Lemma nth_app_r : forall k A (d:A) (L1 L2:list A),
(k >= LibList.length L1)%nat ->
nth_def d k (L1 ++ L2) = nth_def d (k - LibList.length L1) L2.
Proof using.
intros k; induction k; introv N.
{ asserts: (L1 = nil). applys length_zero_inv. math.
subst. rew_list. fequals. }
{ destruct L1 as [|x L1'].
{ rew_list. fequals. }
{ rew_list in *. simpl. applys IHk. math. } }
Qed.
Lemma read_app : forall A `{IA:Inhab A} i (L1 L2 : list A),
(L1 ++ L2)[i] = If i < length L1 then L1[i] else L2[i-length L1].
Admitted.
(* will be proved in TLC for Coq 8.6
Proof.
intros.
unfold LibBag.read, read_inst, read_impl.
unfold nth. repeat case_if; auto; try solve [ false; math ].
(* TODO: use new TLC lemmas about nth *)
{ applys LibList.Nth_to_nth. applys Nth_app_l.
apply Nth_nth_if_in_length. applys int_nat_lt. rewrite abs_pos; math. }
(* TODO: try using
applys nth_app_l. lets: int_nat_lt. apply int_nat_lt. rewrite abs_pos; math. } *)
{ forwards: (>> abs_pos i). math.
unfold LibList.nth. rewrite nth_app_r. fequals.
applys eq_int_nat. rewrites (>> abs_pos (i - length L1)).
math. rewrite LibListZ_length_def.
sets j:(abs i). skip.
} math.
*)
Lemma update_middle :
forall A i (L1 L2 : list A) x y,
i = length L1 ->
(L1 ++ y :: L2)[i := x] = L1 & x ++ L2.
Proof using. intros. applys* update_app_right_here. Qed.
Lemma length_map : forall A B (l:list A) (f:A->B),
length (map f l) = length l.
Proof using. intros. unfold length. rewrite~ length_map. Qed.
Lemma index_map_eq : forall A B (l:list A) i (f:A->B),
index (map f l) i = index l i.
Proof using. intros. rewrite index_def in *. rewrite~ length_map. Qed.
Lemma index_map : forall A B (l:list A) i (f:A->B),
index l i -> index (map f l) i.
Proof using. intros. rewrite~ index_map_eq. Qed.
Lemma read_map : forall `{IA:Inhab A} `{IB:Inhab B} (l:list A) (i:int) (f:A->B),
index l i ->
(map f l)[i] = f (l[i]).
Proof using.
introv H. rewrite index_def, int_index_def in H.
unfold read_inst, read_impl, nth. simpl. case_if.
{ false; math. }
{ rewrite nth_map. (* TODO: why rewrite @nth_map fails *) auto.
applys int_nat_lt. rewrite abs_pos; math. }
Qed.
Lemma update_map : forall A B (l:list A) (i:int) (x:A) (f:A->B),
index l i ->
map f (l[i := x]) = (map f l)[i := f x].
Proof using.
introv H. rewrite index_def, int_index_def in H.
unfold update_inst, update_impl, update. simpl.
case_if. { false; math. }
{ applys list_update_map. { applys int_nat_lt. rewrite abs_pos; math. } }
Qed.
Section MakeProperties.
Transparent make.
Lemma make_zero : forall A (x : A),
make 0 x = nil.
Proof using.
intros. unfold make. case_if. { false; math. }
asserts_rewrite (abs 0 = 0%nat). { applys eq_int_nat. rewrite abs_pos; math. }
auto.
Qed.
Lemma make_succ_l: forall n A (x : A),
n >= 0 ->
make (n+1) x = x :: make n x.
Proof using.
intros. rewrites <- (>> cons_make (n+1)). math. fequals_rec; math.
Qed.
Lemma make_succ_r: forall n A (x : A),
n >= 0 ->
make (n+1) x = make n x & x.
Proof using.
intros. asserts IA: (Inhab A). applys prove_Inhab x. applys ext_eq.
{ rewrite length_make. rew_list. rewrite length_make.
math. math. math. }
{ intros i Ei. rewrite length_make in Ei; [| math ].
rewrite read_make; [| rewrite int_index_def; math ].
rewrite read_app. case_if as C; (rewrite length_make in C; [|math]).
{ rewrite~ read_make. rewrite int_index_def. math. }
{ rewrite length_make; [|math]. math_rewrite (i-n = 0).
rewrite~ read_zero. } }
Qed.
End MakeProperties. (* TODO *)
(* Hint for LibListZ *)
Hint Rewrite length_map index_map_eq : rew_arr.
End ReadProperties.
Export ReadProperties.
(*----------------------*)
(* BAG *)
(* TODO: remove the ` when migrating to TLC *)
Notation "m `[ x := v ]" := (LibBag.update m x v)
(at level 28, format "m `[ x := v ]", left associativity).
(*----------------------*)
(* ListExec *)
Require Import LibLogic. (* needed? *)
Require Import LibReflect.
(* TODO: LibListExec : is_not_nil *)
......@@ -382,46 +139,4 @@ Ltac isbust_core tt :=
Tactic Notation "isubst" :=
isbust_core tt.
(** Auxiliary tactic for obtaining a boolean answer
to the question is E an evar?. *)
Ltac is_evar_as_bool E :=
constr:(ltac:(first
[ is_evar E; exact true
| exact false ])).
Tactic Notation "ltac_set" "(" ident(X) ":=" constr(E) ")" "at" constr(K) :=
match nat_from_number K with
| 1%nat => set (X := E) at 1
| 2%nat => set (X := E) at 2
| 3%nat => set (X := E) at 3
| 4%nat => set (X := E) at 4
| 5%nat => set (X := E) at 5
| 6%nat => set (X := E) at 6
| 7%nat => set (X := E) at 7
| 8%nat => set (X := E) at 8
| 9%nat => set (X := E) at 9
| 10%nat => set (X := E) at 10
| 11%nat => set (X := E) at 11
| 12%nat => set (X := E) at 12
| 13%nat => set (X := E) at 13
| _ => fail "ltac_set: arity not supported"
end.
Ltac generalize_all_prop ::=
repeat match goal with H: ?T |- _ =>
try match T with ltac_Mark => fail 2 end;
match type of T with Prop =>
generalizes H
end end.
Ltac gen_until_mark_with_processing cont :=
match goal with H: ?T |- _ =>
match T with
| ltac_Mark => clear H
| _ => cont H; generalize H; clear H;
gen_until_mark_with_processing cont
end end.
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment