Require Import List.

  bit ::= 0 | 1

  binary_string ::= bit | binary_string bit

  parens ::= () | ( parens ) | parens parens

  x ::= x

Definition name := nat.

Inductive expr : Set :=
| const : nat -> expr
| var : name -> expr
| add : expr -> expr -> expr
| mul : expr -> expr -> expr.

Fixpoint nconsts (e: expr) : nat :=
  match e with
    | const _ => 1
    | var _ => 0
    | add l r => (nconsts l) + (nconsts r)
    | mul l r => (nconsts l) + (nconsts r)
  end.

Lemma has_3_consts:
  exists e, nconsts e = 3.
Proof.
  exists (add (const 1) (add (const 2) (const 3))). simpl. reflexivity.
Qed.

Print orb.

Fixpoint has_const (e: expr) : bool :=
  match e with
    | const _ => true
    | var _ => false
    | add l r => orb (has_const l) (has_const r)
    | mul l r => orb (has_const l) (has_const r)
  end.

Fixpoint has_var (e: expr) : bool :=
  match e with
    | const _ => false
    | var _ => true
    | add l r => orb (has_var l) (has_var r)
    | mul l r => orb (has_var l) (has_var r)
  end.

Lemma bottom_out:
  forall e, has_const e = true \/
            has_var e = true.
Proof.
  intro. induction e.
  { firstorder. }
  { firstorder. }
  { simpl. firstorder. }
  { simpl. firstorder. }
Qed.

Inductive yo: Type :=
| yolo : yo -> yo.

Lemma whack:
  yo -> False.
Proof.
  intro. induction H. destruct IHyo.
Qed.

Print expr_ind.