Commit 7bb59738 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Realize some additional theories in Coq.

parent 6b0c7b82
......@@ -828,7 +828,7 @@ COQLIBS_SET = $(addprefix lib/coq/set/, $(COQLIBS_SET_FILES))
COQLIBS_MAP_FILES = Map MapPermut
COQLIBS_MAP = $(addprefix lib/coq/map/, $(COQLIBS_MAP_FILES))
COQLIBS_LIST_FILES = List Length Mem Nth NthLength HdTl NthHdTl Append
COQLIBS_LIST_FILES = List Length Mem Nth NthLength HdTl NthHdTl Append NthLengthAppend Reverse
COQLIBS_LIST = $(addprefix lib/coq/list/, $(COQLIBS_LIST_FILES))
COQLIBS_OPTION_FILES = Option
......
......@@ -285,6 +285,12 @@ theory list.Append
end
theory list.Reverse
syntax function reverse "(List.rev %1)"
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.Nth.
Require option.Option.
Require list.NthLength.
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)).
Proof.
intros a a_WT l1.
induction l1 as [|x l1].
intros l2 i.
apply NthLength.nth_none_1.
intros l2 i Hi.
simpl.
generalize (Zeq_bool_if i 0).
case Zeq_bool.
easy.
intros _.
apply IHl1.
assert (i < 1 + Length.length l1)%Z by exact Hi.
omega.
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)).
Proof.
intros a a_WT l1.
induction l1 as [|x l1].
intros l2 i _.
simpl.
now rewrite Zminus_0_r.
intros l2 i.
change (Length.length (x :: l1)) with (1 + Length.length l1)%Z.
intros Hi.
replace (i - (1 + Length.length l1))%Z with ((i - 1) - Length.length l1)%Z by ring.
simpl.
generalize (Zeq_bool_if i 0).
case Zeq_bool.
intros Hi'.
generalize (Length.Length_nonnegative l1).
omega.
intros _.
apply IHl1.
omega.
Qed.
(* 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 reverse_def {a:Type} {a_WT:WhyType a}: forall (l:(list a)),
((List.rev l) = match l with
| nil => nil
| (cons x r) => (List.app (List.rev r) (cons x nil))
end).
Proof.
now intros [|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 (cons x l1)) l2) = (List.app (List.rev l1) (cons x l2))).
Proof.
intros a a_WT l1 l2 x.
simpl.
now rewrite <- List.app_assoc.
Qed.
(* Why3 goal *)
Lemma reverse_reverse : forall {a:Type} {a_WT:WhyType a},
forall (l:(list a)), ((List.rev (List.rev l)) = l).
Proof.
intros a a_WT l.
apply List.rev_involutive.
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)).
Proof.
intros a a_WT l.
rewrite 2!Length.length_std.
now rewrite List.rev_length.
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