Commit f9bddf3d by Loïc Correnson Committed by François Bobot

### [wp] remove unused theory dir

parent 0ed2cc2b
 why3shapes.gz
 # Implementation Validation (Parts) To run the proofs: ``` why3 ide proofs ```
 (* Formulae *) theory F use import bool.Bool type a predicate atom a type p = A a | AND p p | OR p p | NOT p | T | F predicate sem (f : p) = match f with | T -> true | F -> false | A a -> atom a | AND u v -> sem u /\ sem v | OR u v -> sem u \/ sem v | NOT u -> not (sem u) end predicate imply (u v : p) = sem u -> sem v function select a : bool function filter (polarity : bool) (f : p) : p = match f with | T -> T | F -> F | A a -> if select a then A a else if polarity then F else T | AND p q -> AND (filter polarity p) (filter polarity q) | OR p q -> OR (filter polarity p) (filter polarity q) | NOT p -> NOT (filter (not polarity) p) end predicate filtering (f : p) = imply (filter true f) f /\ imply f (filter false f) lemma f_true : filtering T lemma f_false : filtering F lemma f_atom : forall a. filtering (A a) lemma f_not : forall p. filtering p -> filtering (NOT p) lemma f_and : forall p q. filtering p -> filtering q -> filtering (AND p q) lemma f_or : forall p q. filtering p -> filtering q -> filtering (OR p q) lemma filtering : forall p. filtering p (* by induction with Coq *) end
 (* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import BuiltIn. Require BuiltIn. Require bool.Bool. Axiom a : Type. Parameter a_WhyType : WhyType a. Existing Instance a_WhyType. Parameter atom: a -> Prop. (* Why3 assumption *) Inductive p := | A : a -> p | AND : p -> p -> p | OR : p -> p -> p | NOT : p -> p | T : p | F : p. Axiom p_WhyType : WhyType p. Existing Instance p_WhyType. (* Why3 assumption *) Fixpoint sem (f:p) {struct f}: Prop := match f with | T => True | F => False | (A a1) => (atom a1) | (AND u v) => (sem u) /\ (sem v) | (OR u v) => (sem u) \/ (sem v) | (NOT u) => ~ (sem u) end. (* Why3 assumption *) Definition imply (u:p) (v:p): Prop := (sem u) -> (sem v). Parameter select: a -> bool. Parameter filter: bool -> p -> p. Axiom filter_def : forall (polarity:bool) (f:p), match f with | T => ((filter polarity f) = T) | F => ((filter polarity f) = F) | (A a1) => (((select a1) = true) -> ((filter polarity f) = (A a1))) /\ ((~ ((select a1) = true)) -> (((polarity = true) -> ((filter polarity f) = F)) /\ ((~ (polarity = true)) -> ((filter polarity f) = T)))) | (AND p1 q) => ((filter polarity f) = (AND (filter polarity p1) (filter polarity q))) | (OR p1 q) => ((filter polarity f) = (OR (filter polarity p1) (filter polarity q))) | (NOT p1) => ((~ (polarity = true)) -> ((filter polarity f) = (NOT (filter true p1)))) /\ ((polarity = true) -> ((filter polarity f) = (NOT (filter false p1)))) end. (* Why3 assumption *) Definition filtering (f:p): Prop := (imply (filter true f) f) /\ (imply f (filter false f)). Axiom f_true : (filtering T). Axiom f_false : (filtering F). Axiom f_atom : forall (a1:a), (filtering (A a1)). Axiom f_not : forall (p1:p), (filtering p1) -> (filtering (NOT p1)). Axiom f_and : forall (p1:p) (q:p), (filtering p1) -> ((filtering q) -> (filtering (AND p1 q))). Axiom f_or : forall (p1:p) (q:p), (filtering p1) -> ((filtering q) -> (filtering (OR p1 q))). (* Why3 goal *) Theorem filtering1 : forall (p1:p), (filtering p1). (* Why3 intros p1. *) intros p. induction p. - apply f_atom. - apply f_and ; auto. - apply f_or ; auto. - apply f_not ; auto. - apply f_true. - apply f_false. Qed.

Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!