coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jonas Oberhauser <s9joober AT gmail.com>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] automating consecutive branches
- Date: Sun, 09 Feb 2014 15:35:02 +0100
I'm trying to automatize the following (ugly) lemma in the attached proof:
Goal (MCDC (fun s => s = s1 \/ s = s2 \/ s = s3 \/ s = s4 \/ s = s5 \/ s = s6) (fun g => g = f)).
hnf.
simpl.
intros [] g eq ; subst.
exists s1 ; exists s6 ;
simpl ; intuition ; try discriminate ;
destruct y ; try (exfalso ; now apply H) ; compute ; intuition.
exists s1 ; exists s6 ;
simpl ; intuition ; try discriminate ;
destruct y ; try (exfalso ; now apply H) ; compute ; intuition.
exists s1 ; exists s5 ;
simpl ; intuition ; try discriminate ;
destruct y ; try (exfalso ; now apply H) ; compute ; intuition.
exists s1 ; exists s5 ;
simpl ; intuition ; try discriminate ;
destruct y ; try (exfalso ; now apply H) ; compute ; intuition.
exists s1 ; exists s4 ;
simpl ; intuition ; try discriminate ;
destruct y ; try (exfalso ; now apply H) ; compute ; intuition.
Qed.
I was trying something along the lines of
(exists s1 || exists s2 || exists s3) ; (exists s4 || exists s5 || exists s6) ; (simpl ; .... ; intuition).
However, since all the exist commands on their own will go through and the "stuckedness" is only discovered much later in the tactic, || does not work.
How can I automatize the script such that I don't have to find the instances for the exists by hand?
Kind regards, Jonas
Inductive Input := A | B | C | D | E.
Definition Assignment := Input -> bool.
Inductive BranchCondition :=
| i : Input -> BranchCondition
| and : BranchCondition -> BranchCondition -> BranchCondition
| not : BranchCondition -> BranchCondition.
Implicit Types x y z : Input.
Implicit Types f g h : BranchCondition.
Implicit Types s t u : Assignment.
Fixpoint apply f s :=
match f with
| i x => s x
| and g h => andb (apply g s) (apply h s)
| not g => negb (apply g s)
end.
Coercion apply : BranchCondition >-> Funclass.
Definition Suite := Assignment -> Prop.
Definition Branch := BranchCondition -> Prop.
Definition inp_eq_dec : forall x y, {x=y} + {x<>y}.
decide equality. Defined.
Definition update s x b := fun y => if inp_eq_dec x y then b else s y.
Definition MCDC (suite : Suite) (branch : Branch) := forall x f, branch f ->
exists s t, suite s /\ suite t /\
f s <> f t
/\ s x <> t x
/\ forall y, y <> x ->
s y = t y
\/ f s = f (update s y (t y))
\/ f t = f (update t y (s y)).
Infix "&&" := and.
Notation "/ x" := (not x).
Definition or f g := /(/f && /g).
Infix "||" := or.
Coercion i : Input >-> BranchCondition.
Definition f := (((A || B) && C) || D) && E.
Definition s1 x := match x with
| A => true
| B => true
| C => true
| D => true
| E => true
end.
Definition s2 x := match x with
| A => false
| B => true
| C => true
| D => true
| E => true
end.
Definition s3 x := match x with
| A => true
| B => true
| C => false
| D => true
| E => true
end.
Definition s4 x := match x with
| A => true
| B => true
| C => true
| D => true
| E => false
end.
Definition s5 x := match x with
| A => true
| B => true
| C => false
| D => false
| E => true
end.
Definition s6 x := match x with
| A => false
| B => false
| C => true
| D => false
| E => true
end.
Goal (MCDC (fun s => s = s1 \/ s = s2 \/ s = s3 \/ s = s4 \/ s = s5 \/ s =
s6) (fun g => g = f)).
hnf.
simpl.
intros [] g eq ; subst.
exists s1 ; exists s6 ;
simpl ; intuition ; try discriminate ;
destruct y ; try (exfalso ; now apply H) ; compute ; intuition.
exists s1 ; exists s6 ;
simpl ; intuition ; try discriminate ;
destruct y ; try (exfalso ; now apply H) ; compute ; intuition.
exists s1 ; exists s5 ;
simpl ; intuition ; try discriminate ;
destruct y ; try (exfalso ; now apply H) ; compute ; intuition.
exists s1 ; exists s5 ;
simpl ; intuition ; try discriminate ;
destruct y ; try (exfalso ; now apply H) ; compute ; intuition.
exists s1 ; exists s4 ;
simpl ; intuition ; try discriminate ;
destruct y ; try (exfalso ; now apply H) ; compute ; intuition.
Qed.
- [Coq-Club] automating consecutive branches, Jonas Oberhauser, 02/09/2014
- Re: [Coq-Club] automating consecutive branches, Justus Matthiesen, 02/09/2014
- Re: [Coq-Club] automating consecutive branches, Adam Chlipala, 02/09/2014
- Re: [Coq-Club] automating consecutive branches, Arnaud Spiwack, 02/10/2014
- Re: [Coq-Club] automating consecutive branches, Justus Matthiesen, 02/09/2014
Archive powered by MHonArc 2.6.18.