# Library POCS.Helpers.Helpers

Require Import Arith.

Require Import Bool.

Require Import List.

Require Import EquivDec.

Set Implicit Arguments.

Require Import Bool.

Require Import List.

Require Import EquivDec.

Set Implicit Arguments.

# Decidable equality.

Here, we define some types for which we know how to compute
decidable equality (namely, equality for nats, and equality
for bools).

Instance nat_equal_dec : EqualDec nat := eq_nat_dec.

Instance bool_equal_dec : EqualDec bool := bool_dec.

# maybe_holds predicate.

Definition maybe_holds T (p:T -> Prop) : option T -> Prop :=

fun mt => match mt with

| Some t => p t

| None => True

end.

Theorem holds_in_none_eq : forall T (p:T -> Prop) mt,

mt = None ->

maybe_holds p mt.

Theorem holds_in_some : forall T (p:T -> Prop) (v:T),

p v ->

maybe_holds p (Some v).

Theorem holds_in_some_eq : forall T (p:T -> Prop) (v:T) mt,

mt = Some v ->

p v ->

maybe_holds p mt.

Theorem holds_some_inv_eq : forall T (p: T -> Prop) mt v,

mt = Some v ->

maybe_holds p mt ->

p v.

Theorem pred_weaken : forall T (p p': T -> Prop) mt,

maybe_holds p mt ->

(forall t, p t -> p' t) ->

maybe_holds p' mt.

To reflect the expected usage of this primitive, we define
two notations:

- mv ?|= p states that p holds on mv, if mv is present.
This notation simply translates to maybe_holds p mv.
- To state that an optional value is definitely missing, we provide a predicate missing, so that mv ?|= missing implies that mv is None. The missing predicate is simply False, which allows us to conclude by contradiction that there's no way the optional value could be Some x.

Notation "m ?|= F" := (maybe_holds F m) (at level 20, F at level 50).

Definition missing {T} : T -> Prop := fun _ => False.

Theorem pred_missing : forall T (p: T -> Prop) mt,

mt ?|= missing ->

mt ?|= p.

# Proof automation.

## Simplify matches when possible

Ltac simpl_match :=

let repl_match_goal d d' :=

replace d with d';

lazymatch goal with

| [ |- context[match d' with _ => _ end] ] => fail

| _ => idtac

end in

let repl_match_hyp H d d' :=

replace d with d' in H;

lazymatch type of H with

| context[match d' with _ => _ end] => fail

| _ => idtac

end in

match goal with

| [ Heq: ?d = ?d' |- context[match ?d with _ => _ end] ] =>

repl_match_goal d d'

| [ Heq: ?d' = ?d |- context[match ?d with _ => _ end] ] =>

repl_match_goal d d'

| [ Heq: ?d = ?d', H: context[match ?d with _ => _ end] |- _ ] =>

repl_match_hyp H d d'

| [ Heq: ?d' = ?d, H: context[match ?d with _ => _ end] |- _ ] =>

repl_match_hyp H d d'

end.

Module SimplMatchTests.

test simpl_match failure when match does not go away

Theorem fails_if_match_not_removed :

forall (vd m: nat -> option nat) a,

vd a = m a ->

vd a = match (m a) with

| Some v => Some v

| None => None

end.

Theorem removes_match :

forall (vd m: nat -> option nat) a v v',

vd a = Some v ->

m a = Some v' ->

vd a = match (m a) with

| Some _ => Some v

| None => None

end.

forall (vd m: nat -> option nat) a,

vd a = m a ->

vd a = match (m a) with

| Some v => Some v

| None => None

end.

Theorem removes_match :

forall (vd m: nat -> option nat) a v v',

vd a = Some v ->

m a = Some v' ->

vd a = match (m a) with

| Some _ => Some v

| None => None

end.

hypothesis replacement should remove the match or fail

Theorem fails_on_hyp_if_match_not_removed :

forall (vd m: nat -> option nat) a,

vd a = m a ->

m a = match (m a) with

| Some v => Some v

| None => None

end ->

True.

End SimplMatchTests.

forall (vd m: nat -> option nat) a,

vd a = m a ->

m a = match (m a) with

| Some v => Some v

| None => None

end ->

True.

End SimplMatchTests.

Ltac destruct_matches_in e :=

lazymatch e with

| context[match ?d with | _ => _ end] =>

destruct_matches_in d

| _ => destruct e eqn:?; intros

end.

Ltac destruct_all_matches :=

repeat (try simpl_match;

try match goal with

| [ |- context[match ?d with | _ => _ end] ] =>

destruct_matches_in d

| [ H: context[match ?d with | _ => _ end] |- _ ] =>

destruct_matches_in d

end);

subst;

try congruence;

auto.

Ltac destruct_nongoal_matches :=

repeat (try simpl_match;

try match goal with

| [ H: context[match ?d with | _ => _ end] |- _ ] =>

destruct_matches_in d

end);

subst;

try congruence;

auto.

Ltac destruct_goal_matches :=

repeat (try simpl_match;

match goal with

| [ |- context[match ?d with | _ => _ end] ] =>

destruct_matches_in d

end);

try congruence;

auto.

Module DestructMatchesTests.

Theorem removes_absurdities :

forall b1 b2,

b1 = b2 ->

match b1 with

| true => match b2 with

| true => True

| false => False

end

| false => match b2 with

| true => False

| false => True

end

end.

Theorem destructs_innermost_match :

forall b1 b2,

match (match b2 with

| true => b1

| false => false

end) with

| true => b1 = true

| false => b1 = false \/ b2 = false

end.

End DestructMatchesTests.

Ltac destruct_tuple :=

match goal with

| [ H: context[let '(a, b) := ?p in _] |- _ ] =>

let a := fresh a in

let b := fresh b in

destruct p as [a b]

| [ |- context[let '(a, b) := ?p in _] ] =>

let a := fresh a in

let b := fresh b in

destruct p as [a b]

end.

Tactic Notation "destruct" "matches" "in" "*" := destruct_all_matches.

Tactic Notation "destruct" "matches" "in" "*|-" := destruct_nongoal_matches.

Tactic Notation "destruct" "matches" := destruct_goal_matches.

Ltac safe_intuition_then t :=

repeat match goal with

| [ H: _ /\ _ |- _ ] =>

destruct H

| [ H: ?P -> _ |- _ ] =>

lazymatch type of P with

| Prop => specialize (H ltac:(t))

| _ => fail

end

| _ => progress t

end.

Tactic Notation "safe_intuition" := safe_intuition_then ltac:(auto).

Tactic Notation "safe_intuition" tactic(t) := safe_intuition_then t.

Ltac destruct_ands :=

repeat match goal with

| [ H: _ /\ _ |- _ ] =>

destruct H

end.

Ltac deex :=

match goal with

| [ H : exists (varname : _), _ |- _ ] =>

let newvar := fresh varname in

destruct H as [newvar ?]; destruct_ands; subst

end.

Module DeexTests.

Theorem chooses_name :

(exists (foo:unit), foo=foo) ->

True.

Theorem chooses_fresh_name :

forall (foo:bool),

(exists (foo:unit), foo=foo) -> True.

End DeexTests.

Ltac descend :=

repeat match goal with

| |- exists _, _ => eexists

end.

Ltac sigT_eq :=

match goal with

| [ H: existT ?P ?a _ = existT ?P ?a _ |- _ ] =>

apply Eqdep.EqdepTheory.inj_pair2 in H; subst

end.

substitute variables that are let bindings (these can be created with set
(x:=value) and appear in the context as v := def)

Ltac subst_var :=

repeat match goal with

| [ v := _ |- _ ] => subst v

end.

Ltac solve_false :=

solve [ exfalso; eauto with false ].

Ltac especialize H :=

match type of H with

| forall (x:?T), _ =>

let x := fresh x in

evar (x:T);

specialize (H x);

subst x

end.

Ltac rename_by_type type name :=

match goal with | x : type |- _ => rename x into name end.

repeat match goal with

| [ v := _ |- _ ] => subst v

end.

Ltac solve_false :=

solve [ exfalso; eauto with false ].

Ltac especialize H :=

match type of H with

| forall (x:?T), _ =>

let x := fresh x in

evar (x:T);

specialize (H x);

subst x

end.

Ltac rename_by_type type name :=

match goal with | x : type |- _ => rename x into name end.