Attention une mise à jour du service Gitlab va être effectuée le mardi 18 janvier (et non lundi 17 comme annoncé précédemment) entre 18h00 et 18h30. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes.

Commit 0b005fe5 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

missing Coq and PVS files

parent 28a81816
(|Child_is_son_or_daughter|
(|child_is_son_or_daughter| 0
(|child_is_son_or_daughter-1| NIL 3594646471 ("" (GRIND) NIL NIL)
((|daughter| CONST-DECL "bool" |Child_is_son_or_daughter| NIL)
(|son| CONST-DECL "bool" |Child_is_son_or_daughter| NIL)
(|child| CONST-DECL "bool" |Child_is_son_or_daughter| NIL)
(|parent| CONST-DECL "bool" |Child_is_son_or_daughter| NIL))
SHOSTAK)))
Child_is_son_or_daughter: THEORY
BEGIN
% do not edit above this line
% Why3 person
person: TYPE+
% Why3 gender
gender: DATATYPE
BEGIN
male: male?
female: female?
END gender
% Why3 gender1
gender1(x:person): gender
% Why3 father
father(x:person): person
% Why3 mother
mother(x:person): person
% Why3 father_gender
father_gender: AXIOM FORALL (p:person): (gender1(father(p)) = male)
% Why3 mother_gender
mother_gender: AXIOM FORALL (p:person): (gender1(mother(p)) = female)
% Why3 parent
parent(p:person, c:person): bool = (p = father(c)) OR (p = mother(c))
% Why3 son
son(s:person, p:person): bool = (gender1(s) = male) AND parent(p, s)
% Why3 daughter
daughter(d:person, p:person): bool = (gender1(d) = female) AND parent(p, d)
% Why3 child
child(c:person, p:person): bool = parent(p, c)
% Why3 child_is_son_or_daughter
child_is_son_or_daughter: THEOREM FORALL (c:person, p:person): child(c,
p) <=> (son(c, p) OR daughter(c, p))
END Child_is_son_or_daughter
\ No newline at end of file
(* This file is generated by Why3's Coq 8.4 driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Axiom person : Type.
Parameter person_WhyType : WhyType person.
Existing Instance person_WhyType.
(* Why3 assumption *)
Inductive gender :=
| Male : gender
| Female : gender.
Axiom gender_WhyType : WhyType gender.
Existing Instance gender_WhyType.
Parameter gender1: person -> gender.
Parameter father: person -> person.
Parameter mother: person -> person.
Axiom Father_gender : forall (p:person), ((gender1 (father p)) = Male).
Axiom Mother_gender : forall (p:person), ((gender1 (mother p)) = Female).
(* Why3 assumption *)
Definition parent (p:person) (c:person): Prop := (p = (father c)) \/
(p = (mother c)).
(* Why3 assumption *)
Definition son (s:person) (p:person): Prop := ((gender1 s) = Male) /\ (parent
p s).
(* Why3 assumption *)
Definition daughter (d:person) (p:person): Prop := ((gender1 d) = Female) /\
(parent p d).
(* Why3 goal *)
Theorem Child_is_son_or_daughter : forall (c:person) (p:person), (parent p
c) <-> ((son c p) \/ (daughter c p)).
(* Why3 intros c p. *)
intros c p.
unfold son, daughter, parent.
split.
intros [h|h].
subst p.
destruct (gender1 c).
left.
split.
trivial.
left.
trivial.
right.
split.
trivial.
left.
trivial.
subst p.
destruct (gender1 c).
left.
split.
trivial.
right.
trivial.
right.
split.
trivial.
right.
trivial.
intros [(h1,h2)|(h1,h2)].
trivial.
trivial.
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