The Coq mailing list

[Jonas Oberhauser <s9joober AT gmail.com>]

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.