Commit 954cd223 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Use fully-qualified names for List.rev and List.app and homogenize Coq equivalence lemmas.

parent 5013a71a
......@@ -304,13 +304,13 @@ end
theory list.Append
syntax function (++) "(List.app %1 %2)"
syntax function (++) "(Init.Datatypes.app %1 %2)"
end
theory list.Reverse
syntax function reverse "(List.rev %1)"
syntax function reverse "(Lists.List.rev %1)"
end
......
......@@ -8,14 +8,15 @@ Require list.Length.
Require list.Mem.
(* Why3 goal *)
Lemma infix_plpl_def {a:Type} {a_WT:WhyType a}: forall (l1:(list a))
Lemma infix_plpl_def : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)),
((List.app l1 l2) = match l1 with
((Init.Datatypes.app l1 l2) = match l1 with
| Init.Datatypes.nil => l2
| (Init.Datatypes.cons x1 r1) => (Init.Datatypes.cons x1 (List.app r1 l2))
| (Init.Datatypes.cons x1 r1) =>
(Init.Datatypes.cons x1 (Init.Datatypes.app r1 l2))
end).
Proof.
now intros [|h1 q1] l2.
now intros a a_WT [|h1 q1] l2.
Qed.
Require Import Lists.List.
......@@ -23,7 +24,7 @@ Require Import Lists.List.
(* Why3 goal *)
Lemma Append_assoc : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)) (l3:(list a)),
((List.app l1 (List.app l2 l3)) = (List.app (List.app l1 l2) l3)).
((Init.Datatypes.app l1 (Init.Datatypes.app l2 l3)) = (Init.Datatypes.app (Init.Datatypes.app l1 l2) l3)).
Proof.
intros a a_WT l1 l2 l3.
apply app_assoc.
......@@ -31,7 +32,7 @@ Qed.
(* Why3 goal *)
Lemma Append_l_nil : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
((List.app l Init.Datatypes.nil) = l).
((Init.Datatypes.app l Init.Datatypes.nil) = l).
Proof.
intros a a_WT l.
apply app_nil_r.
......@@ -40,7 +41,7 @@ Qed.
(* Why3 goal *)
Lemma Append_length : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)),
((list.Length.length (List.app l1 l2)) = ((list.Length.length l1) + (list.Length.length l2))%Z).
((list.Length.length (Init.Datatypes.app l1 l2)) = ((list.Length.length l1) + (list.Length.length l2))%Z).
Proof.
intros a a_WT l1 l2.
rewrite 3!Length.length_std.
......@@ -49,8 +50,9 @@ Qed.
(* Why3 goal *)
Lemma mem_append : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(l1:(list a)) (l2:(list a)), (list.Mem.mem x (List.app l1 l2)) <->
((list.Mem.mem x l1) \/ (list.Mem.mem x l2)).
(l1:(list a)) (l2:(list a)), (list.Mem.mem x
(Init.Datatypes.app l1 l2)) <-> ((list.Mem.mem x l1) \/ (list.Mem.mem x
l2)).
Proof.
intros a a_WT x l1 l2.
split.
......@@ -75,7 +77,7 @@ Qed.
(* Why3 goal *)
Lemma mem_decomp : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(l:(list a)), (list.Mem.mem x l) -> exists l1:(list a), exists l2:(list a),
(l = (List.app l1 (Init.Datatypes.cons x l2))).
(l = (Init.Datatypes.app l1 (Init.Datatypes.cons x l2))).
Proof.
intros a a_WT x l h1.
apply in_split.
......
......@@ -14,7 +14,7 @@ Require list.Append.
(* Why3 goal *)
Lemma nth_append_1 : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)) (i:Z), (i < (list.Length.length l1))%Z -> ((list.Nth.nth i
(List.app l1 l2)) = (list.Nth.nth i l1)).
(Init.Datatypes.app l1 l2)) = (list.Nth.nth i l1)).
Proof.
intros a a_WT l1.
induction l1 as [|x l1].
......@@ -34,7 +34,8 @@ Qed.
(* Why3 goal *)
Lemma nth_append_2 : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)) (i:Z), ((list.Length.length l1) <= i)%Z -> ((list.Nth.nth i
(List.app l1 l2)) = (list.Nth.nth (i - (list.Length.length l1))%Z l2)).
(Init.Datatypes.app l1 l2)) = (list.Nth.nth (i - (list.Length.length l1))%Z
l2)).
Proof.
intros a a_WT l1.
induction l1 as [|x l1].
......
......@@ -9,20 +9,20 @@ Require list.Mem.
Require list.Append.
(* Why3 goal *)
Lemma reverse_def {a:Type} {a_WT:WhyType a}: forall (l:(list a)),
((List.rev l) = match l with
Lemma reverse_def : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
((Lists.List.rev l) = match l with
| Init.Datatypes.nil => Init.Datatypes.nil
| (Init.Datatypes.cons x r) =>
(List.app (List.rev r) (Init.Datatypes.cons x Init.Datatypes.nil))
(Init.Datatypes.app (Lists.List.rev r) (Init.Datatypes.cons x Init.Datatypes.nil))
end).
Proof.
now intros [|x l].
now intros a a_WT [|x l].
Qed.
(* Why3 goal *)
Lemma reverse_append : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)) (x:a),
((List.app (List.rev (Init.Datatypes.cons x l1)) l2) = (List.app (List.rev l1) (Init.Datatypes.cons x l2))).
((Init.Datatypes.app (Lists.List.rev (Init.Datatypes.cons x l1)) l2) = (Init.Datatypes.app (Lists.List.rev l1) (Init.Datatypes.cons x l2))).
Proof.
intros a a_WT l1 l2 x.
simpl.
......@@ -31,7 +31,7 @@ Qed.
(* Why3 goal *)
Lemma reverse_reverse : forall {a:Type} {a_WT:WhyType a},
forall (l:(list a)), ((List.rev (List.rev l)) = l).
forall (l:(list a)), ((Lists.List.rev (Lists.List.rev l)) = l).
Proof.
intros a a_WT l.
apply List.rev_involutive.
......@@ -39,7 +39,7 @@ Qed.
(* Why3 goal *)
Lemma Reverse_length : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
((list.Length.length (List.rev l)) = (list.Length.length l)).
((list.Length.length (Lists.List.rev l)) = (list.Length.length l)).
Proof.
intros a a_WT l.
rewrite 2!Length.length_std.
......
......@@ -770,9 +770,9 @@ let print_equivalence_lemma ~prev info fmt name (ls,ld) =
let _, _, all_ty_params = ls_ty_vars ls in
let def_formula = ls_defn_axiom ld in
fprintf fmt
"(* Why3 goal *)@\n@[<hov 2>Lemma %s %a:@ %a.@]@\n"
"(* Why3 goal *)@\n@[<hov 2>Lemma %s :@ %a%a.@]@\n"
name
(print_tv_binders ~whytypes:true ~implicit:true) all_ty_params
(print_params ~whytypes:true) all_ty_params
(print_expr info) def_formula;
fprintf fmt "%a@\n"
(print_previous_proof (Some (all_ty_params,def_formula)) info) prev
......
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