Commit 5013a71a authored by Guillaume Melquiond's avatar Guillaume Melquiond

Realize list.RevAppend for Coq.

parent 4632cab3
......@@ -868,7 +868,7 @@ COQLIBS_SET = $(addprefix lib/coq/set/, $(COQLIBS_SET_FILES))
COQLIBS_MAP_FILES = Map Occ MapPermut MapInjection
COQLIBS_MAP = $(addprefix lib/coq/map/, $(COQLIBS_MAP_FILES))
COQLIBS_LIST_FILES = List Length Mem Nth NthLength HdTl NthHdTl Append NthLengthAppend Reverse HdTlNoOpt NthNoOpt
COQLIBS_LIST_FILES = List Length Mem Nth NthLength HdTl NthHdTl Append NthLengthAppend Reverse HdTlNoOpt NthNoOpt RevAppend
COQLIBS_LIST = $(addprefix lib/coq/list/, $(COQLIBS_LIST_FILES))
COQLIBS_OPTION_FILES = Option
......
......@@ -314,6 +314,12 @@ theory list.Reverse
end
theory list.RevAppend
syntax function rev_append "(Lists.List.rev_append %1 %2)"
end
theory option.Option
syntax type option "(option %1)"
......
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require list.List.
Require list.Length.
Require list.Mem.
Require list.Append.
(* Why3 goal *)
Lemma rev_append_def : forall {a:Type} {a_WT:WhyType a}, forall (s:(list a))
(t:(list a)),
((Lists.List.rev_append s t) = match s with
| (Init.Datatypes.cons x r) =>
(Lists.List.rev_append r (Init.Datatypes.cons x t))
| Init.Datatypes.nil => t
end).
Proof.
now intros a a_WT [|sh st] t.
Qed.
(* Why3 goal *)
Lemma rev_append_append_l : forall {a:Type} {a_WT:WhyType a},
forall (r:(list a)) (s:(list a)) (t:(list a)),
((Lists.List.rev_append (Init.Datatypes.app r s) t) = (Lists.List.rev_append s (Lists.List.rev_append r t))).
Proof.
intros a a_WT r s.
induction r as [|rh rt IHr].
easy.
now simpl.
Qed.
(* Why3 goal *)
Lemma rev_append_append_r : forall {a:Type} {a_WT:WhyType a},
forall (r:(list a)) (s:(list a)) (t:(list a)),
((Lists.List.rev_append r (Init.Datatypes.app s t)) = (Lists.List.rev_append (Lists.List.rev_append s r) t)).
Proof.
intros a a_WT r s t.
revert r.
induction s as [|sh st IHs].
easy.
intros r.
simpl.
now rewrite <- IHs.
Qed.
(* Why3 goal *)
Lemma rev_append_length : forall {a:Type} {a_WT:WhyType a},
forall (s:(list a)) (t:(list a)),
((list.Length.length (Lists.List.rev_append s t)) = ((list.Length.length s) + (list.Length.length t))%Z).
Proof.
intros a a_WT s.
induction s as [|sh st IHs].
easy.
intros t.
simpl List.rev_append.
rewrite IHs.
change (Length.length (sh :: t)) with (1 + Length.length t)%Z.
change (Length.length (sh :: st)) with (1 + Length.length st)%Z.
ring.
Qed.
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