Code listing for gmalecha.github.io/reflections/2017/2017-02-18-Qed-Considered-Harmful/Qed-Considered-Harmful

QedHarmful.v

Require Import Coq.Lists.List.

Set Implicit Arguments.
Set Strict Implicit.

Section hlist.
  Context {T : Type}.
  Variable F : T -> Type.
  Inductive hlist : list T -> Type :=
  | Hnil : hlist nil
  | Hcons : forall {t ts}, F t -> hlist ts -> hlist (t :: ts).

  Fixpoint hlist_app {ls ls'} (hs : hlist ls) : hlist ls' -> hlist (ls ++ ls') :=
    match hs in hlist ls return hlist ls' -> hlist (ls ++ ls') with
    | Hnil => fun hs' => hs'
    | Hcons h hs => fun hs' => Hcons h (hlist_app hs hs')
    end.

  Theorem hlist_app_assoc
  : forall ls ls' ls''
      (hs : hlist ls) (hs' : hlist ls') (hs'' : hlist ls''),
      hlist_app (hlist_app hs hs') hs'' =
      match eq_sym (app_ass ls ls' ls'') in _ = X return hlist X with
      | eq_refl => hlist_app hs (hlist_app hs' hs'')
      end.
  Proof.
    induction hs.
    { simpl.
      Print app_assoc_reverse.
  Abort.

  Arguments f_equal [_ _ f _ _] _ : clear implicits, rename.

  Fixpoint app_ass_trans ls ls' ls'' : (ls ++ ls') ++ ls'' = ls ++ (ls' ++ ls'') :=
    match ls as ls return (ls ++ ls') ++ ls'' = ls ++ (ls' ++ ls'') with
    | nil => eq_refl
    | l :: ls => f_equal (f:=@cons T l) (app_ass_trans ls ls' ls'')
    end.

  Theorem hlist_app_assoc
  : forall ls ls' ls''
      (hs : hlist ls) (hs' : hlist ls') (hs'' : hlist ls''),
      hlist_app (hlist_app hs hs') hs'' =
      match eq_sym (app_ass_trans ls ls' ls'') in _ = X return hlist X with
      | eq_refl => hlist_app hs (hlist_app hs' hs'')
      end.
  Proof.
    induction hs.
    { simpl. reflexivity. }
    { simpl. intros.
      rewrite IHhs. clear.
      generalize (hlist_app hs (hlist_app hs' hs'')).
      destruct (app_ass_trans ts ls' ls'').
      simpl. reflexivity. }
  Defined.


Section opaque_hlist_app.
  Variable app_ass : forall (xs ys zs : list T), (xs ++ ys) ++ zs = xs ++ (ys ++ zs).

  Theorem hlist_app_assoc
  : forall ls ls' ls''
      (hs : hlist ls) (hs' : hlist ls') (hs'' : hlist ls''),
      hlist_app (hlist_app hs hs') hs'' =
      match eq_sym (app_ass ls ls' ls'') in _ = X return hlist X with
      | eq_refl => hlist_app hs (hlist_app hs' hs'')
      end.
  Proof.
    induction hs.
    { simpl.
  Abort.

End opaque_hlist_app.

Section plus_comm.
  Hypothesis plus_unit : forall a : nat, a + 0 = a.
  Hypothesis plus_S_r : forall a b, a + S b = S (a + b).

  Theorem plus_comm : forall a b : nat, a + b = b + a.
  Proof.
    induction a.
    { intros. symmetry. apply plus_unit. }
    { intros.
      rewrite plus_S_r. simpl; rewrite IHa. reflexivity. }
  Defined.

End plus_comm.

Theorem plus_unit : forall n, n + 0 = n.
Proof.
  induction n; [ reflexivity | simpl; f_equal; assumption ].
Defined.

Theorem plus_S_r : forall a b, a + S b = S (a + b).
Proof.
  induction a.
  { reflexivity. }
  { simpl; intros. f_equal. eapply IHa. }
Defined.

Eval compute in plus_comm plus_unit plus_S_r 5 5.

Opaque plus_unit plus_S_r.

Eval compute in plus_comm plus_unit plus_S_r 5 5.