Create a gist now

Instantly share code, notes, and snippets.

Code listing for gmalecha.github.io/reflections/2017/2017-02-18-Qed-Considered-Harmful/Qed-Considered-Harmful
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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment