Skip to Content.
Sympa Menu

coq-club - [Coq-Club] automating consecutive branches

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] automating consecutive branches


Chronological Thread 
  • 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.




Archive powered by MHonArc 2.6.18.

Top of Page