structural_example.v

Section structural_example.
  Variable A B : Type.
  Variable f g : A -> B.
  Variable Q : B -> Prop.

  Definition eg : Prop := 
    (forall x, Q (g x)) -> 
    (forall x, f x = g x) -> 
    forall x, Q (f x). 


  Lemma eg_vanilla : eg.
  Proof.
    unfold eg.
    intros. 
    rewrite H0. auto.
  Qed.

  Variable R : B -> Prop.

  Definition eg' : Prop := 
    (forall x, Q (g x)) -> 
    (forall x, f x = g x) -> 
    forall x, Q (f x) /\ R (f x).


  Lemma eg'_vanilla_attempt : eg'.
  Proof.
    unfold eg'.
    intros. 
    split.
    - rewrite H0. auto.
    - 
  Admitted.

  Definition eg'' : Prop := 
    (forall x, Q (g x)) -> 
    (forall x, Q (f x) -> R (f x)) -> 
    (forall x, f x = g x) -> 
    forall x, Q (f x) /\ R (f x).


  Lemma eg''_vanilla : eg''.
  Proof.
    intros.
    split.
    - rewrite H1. auto.
    - apply H0. rewrite H1. auto. 
  Qed.

  Require Import JRWTactics.

  Lemma eg_structural : eg.
  Proof.
    unfold eg.
    intros.
    find_higher_order_rewrite.
    auto.
  Qed.

  Lemma eg'_structural_attempt : eg'.
    unfold eg'.
    intros.
    split. 
    - find_higher_order_rewrite. auto.
    - 
  Admitted.

  Ltac find_apply_hyp_goal_no_new_subgoals := 
    match goal with
    | [ H : _ |- _ ] => apply H; [idtac]
    end.

  Lemma eg''_structural : eg''.
  Proof.
    unfold eg''.
    intros.
    split. 
    - find_higher_order_rewrite. auto.
    - find_apply_hyp_goal_no_new_subgoals.
      find_higher_order_rewrite. auto.
  Qed.
End structural_example.