title: Formualting a logic in farmer astronaught
body: <p>There is this logic in a movie which I can't quite formalize (e.g. in Coq).</p>
  
  <p>Some one wanted to launch a rocket on his farm, the FBI guys monitoring the site are talking to one another about why they are there. One guy said:</p>
  
  <blockquote>
    <p>Because if we are not here and he launches, we will look like as*s.</p>
  </blockquote>
  
  <p>Then the other guy responded </p>
  
  <blockquote>
    <p>what if we are here and he launches? </p>
  </blockquote>
  
  <p>answer: </p>
  
  <blockquote>
    <p>we'll still look like as*s.</p>
  </blockquote>
  
  <p>It seems that the logic here is this:
  Given:</p>
  
  <pre><code>A = we look foolish
  B = he launches
  C = we are not here.
  </code></pre>
  
  <p>We have</p>
  
  <pre><code> B /\ C -&gt; A    and
   B /\ ~C -&gt; A
  </code></pre>
  
  <p>Furthermore, it seems that whether <code>C</code> (we are here) holds does not matter. The conclusion boils down to <code>B -&gt; A</code>. (If he launches, we will look foolish).</p>
  
  <p>Can we prove this reasoning?</p>
  
  <p>I tried: </p>
  
  <pre><code>Theorem farmer: forall A B C:Prop, 
  (B /\ C -&gt; A) -&gt; (B /\ ~C -&gt; A) -&gt; (B -&gt; A).
  Proof.
  intros. tauto.
  </code></pre>
  
  <p>Then it's stuck. I tried adding the excluded middle, but <code>tauto</code> still can't prove it. </p>
  
  <p>On the other hand, doing boolean algebra, we have:</p>
  
  <pre><code>(~B + ~C + A)(~B + C + A) = 
  (~B + A)C + (~B + A)~C + (~B +A) =
  ~B + A.
  </code></pre>
  
  <p>i.e.</p>
  
  <pre><code>(B /\ C -&gt; A) /\ (B /\ ~C -&gt; A) = B -&gt; A.
  </code></pre>
  
  <p>How can this be proved in Coq's logic, or did I derive it wrong?</p>