Commit 90214925 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Realize list.Combine for Coq.

parent 954cd223
......@@ -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 RevAppend
COQLIBS_LIST_FILES = List Length Mem Nth NthLength HdTl NthHdTl Append NthLengthAppend Reverse HdTlNoOpt NthNoOpt RevAppend Combine
COQLIBS_LIST = $(addprefix lib/coq/list/, $(COQLIBS_LIST_FILES))
COQLIBS_OPTION_FILES = Option
......
......@@ -320,6 +320,12 @@ theory list.RevAppend
end
theory list.Combine
syntax function combine "(Lists.List.combine %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 list.List.
(* Why3 comment *)
(* combine is replaced with (Lists.List.combine x x1) by the coq driver *)
(* Why3 goal *)
Lemma combine_def : forall {a:Type} {a_WT:WhyType a}
{b:Type} {b_WT:WhyType b}, forall (x:(list a)) (y:(list b)), match (x,
y) with
| ((Init.Datatypes.cons x0 x1), (Init.Datatypes.cons y0 y1)) =>
((Lists.List.combine x y) = (Init.Datatypes.cons (x0,
y0) (Lists.List.combine x1 y1)))
| _ => ((Lists.List.combine x y) = Init.Datatypes.nil)
end.
Proof.
now intros a a_WT b b_WT [|xh xt] [|yh yt].
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