Feb11.v

Set Implicit Arguments.

Require Import Cpdt.CpdtTactics.
Require Import Lists.List Arith.

Module LE.

  Unset Printing Notations.
  Check (forall (n m : nat), { n <= m } + { n > m }).
  Check (forall (n m : nat), n <= m \/ n > m ).

  Print sumbool.
  Print or.
  Print and.
  (* What is the analogous data structure in Set that is analogous to and? *)
  
  Set Printing Notations.

  Lemma le_gt_dec_failed : forall (n m : nat), { n <= m } + { n > m }.
  Proof with crush.
    intros.
    induction n.
    + left. crush.
    + destruct IHn as [H | H].
      - apply le_lt_or_eq in H. 
        try (destruct H).
        admit.
      - crush.
  Defined.

  Print le_gt_dec_failed.

  (* The code below only works when we define a proof. *)
  Print True.
  Print bool.
  Definition reduced (n m : nat) (H : n < m \/ n = m) : True.
    refine (match H with
              | or_introl n_lt_m => _ 
              | or_intror n_eq_m => _
            end).
  Abort.

  Fixpoint le_gt_dec (n m : nat) : { n <= m } + { n > m }.
  refine (match n, m with
            | O, _ => left _
            | S _, O => right _
            | S n', S m' => match le_gt_dec n' m' with
                              | left _ => left _
                              | right _ => right _
                            end
          end).
  crush. crush. crush. crush.
  Defined.

End LE.

Module Propositional.

  Definition var := nat.
  
  Inductive prop : Set :=
  | Var : var -> prop
  | Lit : bool -> prop
  | Neg : prop -> prop
  | And : prop -> prop -> prop
  | Or : prop -> prop -> prop.

  Fixpoint propDenote (truth : var -> bool) (p : prop) : Prop :=
    match p with
      | Var x => truth x = true
      | Lit b => b = true
      | Neg p' => ~ propDenote truth p'
      | And p1 p2 => propDenote truth p1 /\ propDenote truth p2
      | Or p1 p2 => propDenote truth p1 \/ propDenote truth p2
    end.

  Lemma bool_true_dec : forall b, { b = true } + { ~ b = true }.
    destruct 0; crush.
  Qed.

  Lemma decide : forall t p, { propDenote t p } + { ~ propDenote t p }.
  Proof with crush.
    intros t p.
    induction p...
    destruct (bool_true_dec (t v)) as [H | H]...
    destruct b...
  Qed.

  Notation "[ e ]" := (exist _ e _).

  Fixpoint negate (p : prop)
    : { p' : prop | forall t, propDenote t p <-> ~ propDenote t p' }.
  refine (match p with
            | Var x => [ Neg (Var x) ]
            | Lit true => [ Lit false ]
            | Lit false => [ Lit true ]
            | Neg p' => match negate p' with
                          | [ p'' ] => [ Neg p'' ]
                        end
            | And p1 p2 => 
              match negate p1, negate p2 with
                | [  p1' ], [ p2' ] =>
                  [ Or p1' p2' ]
              end
            | Or p1 p2 =>
              match negate p1, negate p2 with
                | [ p1' ], [ p2' ] =>
                  [ And p1' p2' ]
              end
          end).
  + split.
    - crush.
    - destruct (bool_true_dec (t x)) as [H0 | H0]; crush.
  + crush.
  + crush.
  (* What is being "destructed" below? *)
  + intros. destruct (i t). crush.
  + intros. destruct (i t). destruct (i0 t). crush.
  + intros. destruct (i t). destruct (i0 t).
    split. 
    - crush.
    - intros. simpl.
      destruct (decide t p1'); crush.
  Defined.

  Extraction negate.

End Propositional.