Library src.Heq


Heq ver 0.91

Supports for heterogeneous equality.

Author: Chung-Kil Hur

Institution: Laboratoire Preuves Programmes Systemes, CNRS & Universite Paris Diderot

load the tactics "hresolve_core" and "hget_evar" written in ML
Declare ML Module "hresolve".

Require Import Eqdep JMeq.

Set Implicit Arguments.

General Purpose Tactics


destruct tuples and pairs in local context
Ltac destr_pair :=
 match goal with
   | [H : (_ /\ _) |- _] => let H2 := fresh in assert (H2 := proj2 H); apply proj1 in H
   | [H : prod _ _ |- _] => let H2 := fresh in assert (H2 := snd H); apply fst in H
 end.

Ltac destr_pairs := repeat (destr_pair).

Lemma tuple_split: forall (A B:Type) (a a':A) (b b':B), (a,b) = (a',b') -> a = a' /\ b = b'.
intros. inversion H; clear H. auto.
Qed.

Ltac split_tuple := match goal with [H : (_,_) = (_,_) |- _] => apply tuple_split in H end.

Ltac split_tuples := repeat (split_tuple).

Ltac destr_tupairs := repeat (split_tuples; destr_pairs).

variants of assert that choose a fresh name for the newly added hypothesis
Ltac assertF H := let Hq := fresh in assert (Hq := H).
Ltac assertD H := let Hq := fresh in assert (Hq := H); destr_tupairs.

syntactic checks for hypothesis in local context

Ltac check_equal H1 H2 := match H1 with | H2 => idtac end.

Ltac check_not_equal H1 H2 := try (check_equal H1 H2; fail 1).

Tactic Notation "check_hyp" hyp(H) := (idtac).

Ltac check_not_hyp C := try (check_hyp C; fail 1).

Ltac check_def H := match goal with [ Hcrr := _ |- _ ] => check_equal Hcrr H end.

Ltac check_not_def H := try (check_def H; fail 1).

get_concl and get_type

Ltac get_concl := lazymatch goal with [ |- ?G ] => G end.

Ltac get_hyp H := match goal with [ Hcrr : ?G |- _ ] => match Hcrr with H => G end end.

clear hypothesis upto H, clear identity equations, clear duplicated (syntactically equal) hypothesis

Ltac clear_upto H :=
  repeat (match goal with [Hcrr : _ |- _ ] => first [ check_equal Hcrr H; fail 2 | clear Hcrr ] end).

Ltac clear_idhyps := repeat (match goal with [ H : @eq _ ?X ?Y |- _ ] => unify X Y; clear H end).

Ltac clear_duphyps := repeat (
  match reverse goal with | [ H : ?X |- _ ] =>
      match goal with | [ H' : ?Y |- _ ] =>
          match H with
            | H' => fail 2
            | _ => check_equal X Y ; (clear H' || clear H)
          end
      end
  end).

the same as inversion, but does not touch the conclusion of the goal
Ltac inversion_eq H :=
 (let temp := fresh "_temp_" in
    lazymatch goal with [ |- ?G ] => remember G as temp end;
    lazymatch goal with [ temp_eq : _ |- _ ] => inversion H; rewrite temp_eq; clear temp_eq; clear temp end).

Ltac inversion_eq_clear H :=
 (let temp := fresh "_temp_" in
    assert(temp := I);
    let X := get_hyp H in
      inversion_eq H;
      first [
        match goal with [ Hcrr : ?Y |- _ ] => first [ check_equal Hcrr temp; fail 2 | unify X Y; clear Hcrr ] end |
        clear H ];
    clear temp).

Definitions and Lemmas for Heq


Definition of Heq

Definition HType := Type.
Definition HId (A:HType) : HType := A.

Notation "t1 =t= t2" := (@eq HType t1 t2) (at level 50).
Definition htyeq t1 t2 := (t1 =t= t2).

Notation "{{ Sig # u , a }}" := (@existT _ Sig u a) (at level 50).
Notation "{{{ u , a }}}" := (@existT HType HId u a) (at level 50).

Definition Heq (U:Type) (Sig: U -> Type) (u:U) (a:Sig u) (v:U) (b:Sig v) : Prop := {{ Sig # u , a }} = {{ Sig # v , b }}.

Implicit Arguments Heq [U u v].

Notation "{{ Sig , u , v # a == b }}" := (@Heq _ Sig u a v b) (at level 50, only parsing).
Notation "{{ Sig , Pat # a == b }}" := (@Heq _ Sig Pat a Pat b) (at level 50, only parsing).
Notation "{{ Sig # a == b }}" := (Heq Sig a b) (at level 50).
Notation "{{{ a == b }}}" := (Heq (U:=HType) HId a b) (at level 50).

Definition of hcast

Definition hcast (U : Type) (Sig : U -> Type) (u v : U) (pf : u = v) (a : Sig u) : Sig v := @eq_rect U u Sig a v pf.

Implicit Arguments hcast [U v].

Notation "<< Sig , u # C >> a" := (hcast Sig u C a) (right associativity, at level 65, only parsing).
Notation "<< Sig # C >> a" := (hcast Sig _ C a) (right associativity, at level 65).
Notation "<<< C >>> a" := (hcast (U:=HType) HId _ C a) (right associativity, at level 65).

Basic lemmas for Heq


folding Heq

Lemma Heq_fold: forall (U:Type) (Sig: U -> Type) (u:U) (a:Sig u) (v:U) (b:Sig v), ({{Sig # u,a}} = {{Sig # v,b}}) = {{ Sig # a == b }}. auto. Defined.
Hint Rewrite Heq_fold : Heq_fold.

Ltac Heq_fold :=
  destr_tupairs;
  repeat (match goal with [H : @existT ?X ?Sig ?x ?a = @existT _ _ ?y ?b |- _] => fold (@Heq X Sig x a y b) in H end);
  autorewrite with Heq_fold in *.

Heq is a generalization of eq

Lemma eq_Heq: forall (U:Type) (Sig: U -> Type) (u:U) (a b:Sig u), a = b -> {{ Sig # a == b }}.
intros. subst. red. auto.
Defined.
Implicit Arguments eq_Heq [U a b].

Lemma eq_HeqI: forall (A:HType) (a b: A), a = b -> {{{ a == b }}}.
apply eq_Heq.
Defined.

Hint Resolve eq_Heq eq_HeqI.

Lemma Heq_eq : forall (U:Type) (Sig: U -> Type) (u:U) (a b:Sig u), {{ Sig # a == b }} -> a = b.
apply inj_pairT2.
Defined.
Implicit Arguments Heq_eq [U a b].

Lemma Heq_eqI : forall (U:HType) (a b: U), {{{ a == b }}} -> a = b. apply Heq_eq. Qed.

Heq is an equivalence relation

Lemma refl_Heq : forall (U:Type) (Sig: U -> Type) (u:U) (a:Sig u), {{ Sig # a == a }}. reflexivity. Defined.

Lemma sym_Heq : forall (U:Type) (Sig: U -> Type) (u:U) (a:Sig u) (v:U) (b:Sig v), {{ Sig # a == b }} -> {{ Sig # b == a }}.
intros. red in H. dependent rewrite H. reflexivity.
Defined.

Lemma trans_Heq : forall (U:Type) (Sig: U -> Type) u (a:Sig u) v (b:Sig v) w (c:Sig w),
  {{ Sig # a == b }} -> {{ Sig # b == c }} -> {{ Sig # a == c }}.
intros. red in H, H0. dependent rewrite H. dependent rewrite H0. reflexivity.
Defined.

Hint Resolve refl_Heq sym_Heq trans_Heq.

destruction and construction of Heq

Lemma Heq_proj1 : forall (U:Type) (Sig: U -> Type) (u:U) (a:Sig u) (v:U) (b:Sig v), {{ Sig # a == b }} -> u = v.
intros. red in H. inversion H. reflexivity.
Defined.
Implicit Arguments Heq_proj1 [U Sig u a v b].

Lemma Heq_proj2 : forall (U:Type) (Sig: U -> Type) (u:U) (a:Sig u) (v:U) (b:Sig v), {{ Sig # a == b }} -> {{{ a == b }}}.
intros. red in H. inversion H. reflexivity.
Defined.
Implicit Arguments Heq_proj2 [U a b].

Lemma Heq_split : forall (U:Type) (Sig: U -> Type) (u:U) (a:Sig u) (v:U) (b:Sig v), u = v -> {{{ a == b }}} -> {{ Sig # a == b }}.
intros. subst. apply Heq_eq in H0. subst. auto.
Qed.

relationship between Heq and sigT

Lemma sigT_eta: forall (U:Type) (Sig: U -> Type) (x: sigT Sig), x = {{ Sig # projT1 x , projT2 x }}.
destruct x; reflexivity.
Defined.

Lemma Heq_sigT: forall (U:Type) (Sig:U -> Type) (x y : sigT Sig), {{ Sig # projT2 x == projT2 y }} -> x = y.
intros. rewrite (sigT_eta x), (sigT_eta y). apply H.
Defined.

Heq is a generalization of JMeq

Lemma Heq_JMeq : forall (A B:Type) (a:A) (b:B), {{{ a == b }}} <-> JMeq a b.
split; intros; [red in H; dependent rewrite H | case H]; auto.
Qed.

Heq is equivalent to eq_dep

Lemma Heq_eq_dep : forall (U:Type) (Sig: U -> Type) (u:U) (a:Sig u) (v:U) (b:Sig v), {{ Sig # a == b }} <-> eq_dep _ Sig _ a _ b.
split; intros; [red in H; dependent rewrite H | case H]; auto.
Qed.

Tactics for Heq


Internal Use: hresolve_pre, hresove_post, hresolve_constr

Definition hresolve_arg (A:Type) (a:A) := True.

Ltac hresolve_pre C T tac_resolve :=
 (let hT := fresh "_temp_" in
    assert (hT : hresolve_arg T) by (exact I);
  let hx := fresh "hx" in
    set (hx := C) in hT;
    lazymatch goal with [ _ : @hresolve_arg _ ?T' |- _ ] => tac_resolve hx T' end;
    clear hT ;
  let hf := fresh "hf" in
    intro hf).

Ltac hresolve_post tac :=
 (lazymatch goal with [ hf := ?T' |- _ ] => clear hf;
    lazymatch goal with [ hx := _ |- _ ] => tac T' hx; try (clear hx) end
  end).

Tactic Notation "hresolve_constr" constr(C) "at" int_or_var(occ) "in" constr(T) :=
  hresolve_pre C T ltac:(fun hx T' => hresolve_core (hx := C) at occ in T').

Tactic Notation "hresolve_constr" constr(C) "in" constr(T) :=
  hresolve_pre C T ltac:(fun hx T' => hresolve_core (hx := C) in T').

* hresolve C ( at occ ) ( in H )

finds all occurrences of C in the conclusion (or in the hypothesis H) that are dependent with the occ-th occurrence of C, and replaces the occrences with a new local definition "hx" of C.

* hresolve C ( in H)

is equivalent to first [ hresolve C at 1 (in H) | hresolve C at 2 (in H) | ... | hresolve C at n (in H) ] for n the last occurrene of C.

Tactic Notation "hresolve" constr(C) "at" int_or_var(occ) :=
 (let G := get_concl in hresolve_constr C at occ in G; hresolve_post ltac:(fun G' hx => change G')).

Tactic Notation "hresolve" constr(C) :=
 (let G := get_concl in hresolve_constr C in G; hresolve_post ltac:(fun G' hx => change G')).

Tactic Notation "hresolve" constr(C) "at" int_or_var(occ) "in" hyp(H) :=
 (let G := get_hyp H in hresolve_constr C at occ in G; hresolve_post ltac:(fun G' hx => change G' in H)).

Tactic Notation "hresolve" constr(C) "in" hyp(H) :=
 (let G := get_hyp H in hresolve_constr C in G; hresolve_post ltac:(fun G' hx => change G' in H)).

* hpattern C ( at occ ) ( in H )

the same as pattern, but abstracts the occ-th and its dependent occurrencies of C in the conclusion (or in the hypothesis H).

Tactic Notation "hpattern" constr(C) "at" int_or_var(occ) :=
 (let G := get_concl in hresolve_constr C at occ in G; hresolve_post ltac:(fun G' hx => change G'; pattern hx; change hx with C)).

Tactic Notation "hpattern" constr(C) :=
 (let G := get_concl in hresolve_constr C in G; hresolve_post ltac:(fun G' hx => change G'; pattern hx; change hx with C)).

Tactic Notation "hpattern" constr(C) "at" int_or_var(occ) "in" hyp(H) :=
 (let G := get_hyp H in hresolve_constr C at occ in G; hresolve_post ltac:(fun G' hx => change G' in H; pattern hx in H; change hx with C in H)).

Tactic Notation "hpattern" constr(C) "in" hyp(H) :=
 (let G := get_hyp H in hresolve_constr C in G; hresolve_post ltac:(fun G' hx => change G' in H; pattern hx in H; change hx with C in H)).

* hgeneralize C ( at occ ) as id

generalizes the occ-th and its dependent occurrences of C

Tactic Notation "hgeneralize" constr(C) "at" int_or_var(occ) "as" ident(id) :=
 (let G := get_concl in hresolve_constr C at occ in G; hresolve_post ltac:(fun G' hx => change G'; generalize hx as id)).

Tactic Notation "hgeneralize" constr(C) "as" ident(id) :=
 (let G := get_concl in hresolve_constr C in G; hresolve_post ltac:(fun G' hx => change G'; generalize hx as id)).

Tactic Notation "hgeneralize_simpl" constr(C) "at" int_or_var(occ) "as" ident(id) :=
 (hgeneralize C at occ as id; intro; lazymatch goal with [ H : _ |- _ ] => simpl in H; revert H end).

Tactic Notation "hgeneralize_simpl" constr(C) "as" ident(id) :=
 (hgeneralize C as id; intro; lazymatch goal with [ H : _ |- _ ] => simpl in H; revert H end).

* hrewrite ( <- ) eqn ( at occ )

rewrites the occ-th and its dependent occurrences of lhs of eqn to rhs of eqn

Ltac hrewrite_with eqn tac_res :=
 (lazymatch (type of eqn) with @eq _ ?X ?Y =>
    let G := get_concl in
      tac_res X G;
      hresolve_post ltac:(fun G' hx =>
        change G'; let Heqn := fresh "_temp_" in assert (Heqn : hx = Y) by (apply eqn); rewrite Heqn; clear Heqn)
  end).

Tactic Notation "hrewrite" constr(eqn) "at" int_or_var(occ) :=
  hrewrite_with eqn ltac:(fun X G => hresolve_constr X at occ in G).

Tactic Notation "hrewrite" "<-" constr(eqn) "at" int_or_var(occ) := (hrewrite (sym_eq eqn) at occ).

Tactic Notation "hrewrite" constr(eqn) :=
  hrewrite_with eqn ltac:(fun X G => hresolve_constr X in G).

Tactic Notation "hrewrite" "<-" constr(eqn) := (hrewrite (sym_eq eqn)).

* heq_rewrite ( <- ) eqn

exactly the same as "dependent rewrite" but also works for Heqs

Ltac heq_rewrite_with eqn tac :=
 (let heq := fresh "_temp_" in assert (heq := eqn); try (red in heq); tac heq; clear heq; simpl projT1; simpl projT2).

Tactic Notation "heq_rewrite" constr(eqn) := (heq_rewrite_with eqn ltac:(fun heq => dependent rewrite heq)).
Tactic Notation "heq_rewrite" "<-" constr(eqn) := (heq_rewrite (sym_Heq eqn)).

* heq_hrewrite ( <- ) eqn ( at occ )

a variant of "dependent rewrite" using "hrewrite" instead of "rewrite". rewrites the occ-th and its dependent occurrences of lhs of eqn to rhs of eqn, for eqn an equation between dependent pairs, or an Heq.

Ltac heq_hrewrite_with eqn tac :=
 (let heq := fresh "_temp_" in
    assert (heq := eqn); try (red in heq);
  lazymatch (type of heq) with @eq _ (@existT ?U ?Sig ?u ?X) (@existT _ _ ?v ?Y) =>
    let hx := fresh "_temp_" in
      set (hx := @existT U Sig u X) in heq;
      change X with (projT2 hx); change u with (projT1 hx);
      tac heq;
      clear heq; unfold hx in *; clear hx;
      simpl projT1; simpl projT2
  end).

Tactic Notation "heq_hrewrite" constr(eqn) "at" int_or_var(occ) :=
  (heq_hrewrite_with eqn ltac:(fun heq => hrewrite heq at occ)).

Tactic Notation "heq_hrewrite" "<-" constr(eqn) "at" int_or_var(occ) := (heq_hrewrite (sym_eq eqn) at occ).

Tactic Notation "heq_hrewrite" constr(eqn) :=
  (heq_hrewrite_with eqn ltac:(fun heq => hrewrite heq)).

Tactic Notation "heq_hrewrite" "<-" constr(eqn) := (heq_hrewrite (sym_eq eqn)).

Internal Use : Hlock_hyp, Hunlock_hyp

Definition HeqLockHyp1 (A : Type) (x : A) := x.
Definition HeqLockHyp2 (A : Type) (x : A) := x.

Ltac Hlock_hyp Idx H :=
  let X := get_hyp H in match X with | Idx _ _ => fail 1 | _ => change X with (Idx _ X) in H end.

Ltac Hlock_hyps_from_top_upto Idx H :=
  repeat (match reverse goal with [ Hcrr : _ |- _ ] => first [ check_equal Hcrr H; fail 2 | Hlock_hyp Idx Hcrr ] end).

Ltac Hlock_hyps_from_top_until Idx H :=
  Hlock_hyps_from_top_upto Idx H; try (Hlock_hyp Idx H).

Ltac Hlock_hyps_from_bottom_upto Idx H :=
  repeat (match goal with [ Hcrr : _ |- _ ] => first [ check_equal Hcrr H; fail 2 | Hlock_hyp Idx Hcrr ] end).

Ltac Hlock_hyps_from_bottom_until Idx H :=
  Hlock_hyps_from_bottom_upto Idx H; try (Hlock_hyp Idx H).

Ltac Hlock_hyps Idx := repeat (match goal with [ Hcrr : _ |- _ ] => Hlock_hyp Idx Hcrr end).

Ltac Hunlock_hyps Idx := unfold Idx in *.

Tactic Notation "Hlock_hyp" "1" hyp(H) := (Hlock_hyp HeqLockHyp1 H).
Tactic Notation "Hlock_hyps_from_top_upto" "1" hyp(H) := (Hlock_hyps_from_top_upto HeqLockHyp1 H).
Tactic Notation "Hlock_hyps_from_top_until" "1" hyp(H) := (Hlock_hyps_from_top_until HeqLockHyp1 H).
Tactic Notation "Hlock_hyps_from_bottom_upto" "1" hyp(H) := (Hlock_hyps_from_bottom_upto HeqLockHyp1 H).
Tactic Notation "Hlock_hyps_from_bottom_until" "1" hyp(H) := (Hlock_hyps_from_bottom_until HeqLockHyp1 H).
Tactic Notation "Hlock_hyps" "1" := (Hlock_hyps HeqLockHyp1).
Tactic Notation "Hunlock_hyps" "1" := (Hunlock_hyps HeqLockHyp1).

Tactic Notation "Hlock_hyp" "2" hyp(H) := (Hlock_hyp HeqLockHyp2 H).
Tactic Notation "Hlock_hyps_from_top_upto" "2" hyp(H) := (Hlock_hyps_from_top_upto HeqLockHyp2 H).
Tactic Notation "Hlock_hyps_from_top_until" "2" hyp(H) := (Hlock_hyps_from_top_until HeqLockHyp2 H).
Tactic Notation "Hlock_hyps_from_bottom_upto" "2" hyp(H) := (Hlock_hyps_from_bottom_upto HeqLockHyp2 H).
Tactic Notation "Hlock_hyps_from_bottom_until" "2" hyp(H) := (Hlock_hyps_from_bottom_until HeqLockHyp2 H).
Tactic Notation "Hlock_hyps" "2" := (Hlock_hyps HeqLockHyp2).
Tactic Notation "Hunlock_hyps" "2" := (Hunlock_hyps HeqLockHyp2).

* Hset_concl

attach a tag to the current conclusion so that the proof search engine can recognize it as a conclusion. This operation is needed when the conclusion includes (heterogeneous) equations.

* Hunset_concl

remove the tag

Definition HSetConcl (A : Type) (x : A) := x.

Ltac Hset_concl := let G := get_concl in change (HSetConcl G).

Ltac Hunset_concl := unfold HSetConcl.

Internal Use : Hset_concl0, Hunset_concl0

Definition HSetConcl0 (A : Type) (x : A) := x.
Ltac Hset_concl0 := let G := get_concl in change (HSetConcl0 G).
Ltac Hunset_concl0 := unfold HSetConcl0.

* Hhide_evars

hide evars in the conclusion

* Hshow_evars

show the hidden evars

Definition HeqEvar (A:Type) (x:A) := x.

Ltac Hhide_evars :=
  (let temp := fresh "_temp_" in
    assert (temp := I);
    repeat (
      hget_evar 1;
      intro; lazymatch goal with [ H := ?X |- _ ] =>
        let hev := fresh "hev0" in set (hev := X) in *; change X with (HeqEvar X) in hev
      end);
    clear_upto temp; clear temp).

Ltac Hshow_evars := repeat (match goal with [ H := @HeqEvar _ _ |- _ ] => unfold HeqEvar in H; unfold H in *; clear H end).

* Hhide_concl

hide the current conclusion

* Hshow_concl

show the hidden conclusion

Definition HHideConcl (A:Type) (x:A) := x.

Ltac Hhide_concl := match goal with [ |- ?G ] => let hconcl := fresh "hconcl" in set (hconcl := G); change G with (HHideConcl G) in hconcl end.

Ltac Hshow_concl := match goal with [ H := @HHideConcl _ _ |- _ ] => unfold HHideConcl in H; unfold H; clear H end.

Internal Use : intro equations

Ltac intro_eq :=
  first [
    match goal with | [ |- HSetConcl0 _ ] => fail 2 | [ |- HSetConcl _ ] => fail 2 end |
    intro; lazymatch goal with [ H : ?X |- _ ] => match X with | @eq _ _ _ => idtac | @Heq _ _ _ _ _ _ => idtac | _ => fail 1 end; simpl in H end ].

Ltac intro_eqs := repeat intro_eq.

Internal Use : revert equations

Ltac revert_eq_upto H :=
  repeat (match goal with [Hcrr : ?X |- _ ] =>
            first [ check_equal Hcrr H; fail 2 |
                    match X with | @eq _ _ _ => revert Hcrr | @Heq _ _ _ _ _ _ => revert Hcrr end ]
          end).

Internal Use : clear equations

Ltac clear_eq_upto H :=
  repeat (match goal with [Hcrr : ?X |- _ ] =>
            first [ check_equal Hcrr H; fail 2 |
                    match X with | @eq _ _ _ => clear Hcrr | @Heq _ _ _ _ _ _ => clear Hcrr end ]
          end).

* Hsubst

Heq version of the "subst" tactic

This can be used to simplify heterogeneous equations generated by the "inversion" tactic.

Definition HeqHint (A:Type) (a:A) (B:Type) (_:B) := a.

Lemma Heq_proj1_conj : forall (U:Type) (Sig: U -> Type) (u:U) (a:Sig u) (v:U) (b:Sig v),
  {{ Sig # a == b }} -> {{ Sig # a == b }} /\ u = v.
intros. assertD (Heq_proj1 H). subst. split; auto.
Qed.

Ltac Hsubst_one :=
  
    Heq_fold; repeat (match goal with [H : @Heq _ _ _ _ _ _ |- _] => first [ apply Heq_proj1_conj in H | assertF H; unfold Heq in H ] end);

  
    repeat (
      destr_tupairs;
      repeat(match goal with [ H : @eq _ _ _ |- _ ] =>
               autorewrite with Heq_rw in H; match goal with [ H' : @HeqHint _ _ _ ?Inj |- _ ] => apply Inj in H' end
             end);
      repeat subst;
      repeat (match goal with [H : @Heq _ _ _ _ _ _ |- _] => apply Heq_eq in H end)
    );

  
    Heq_fold; clear_idhyps; clear_duphyps.

Ltac Hsubst := repeat Hsubst_one.

Internal Use : matchbug_fix

Definition matchbug_sig (_: nat) : Type := True.
Definition matchbug_elmt := I.
Definition matchbug : 0 = 0 := refl_equal 0.
Definition matchbug_fix (T:Type) (G:T) (_:True) : T := G.

Ltac matchbug_begin := let G := get_concl in change (matchbug_fix G (@hcast _ matchbug_sig _ _ matchbug matchbug_elmt)).

Tactic Notation "matchbug_main" tactic(tac) :=
 (let core H := (first [ match H with matchbug => fail 2 end | tac H ]) in
  match goal with
    | [ |- appcontext[ @hcast _ _ _ _ ?H ] ] => core H
  end).

Ltac matchbug_end := unfold matchbug_fix.

* Hgeneralize

generalizes all casts appearing in the conclusion.

Ltac Hgeneralize :=
  matchbug_begin;
  simpl projT1 in *; simpl projT2 in *;
  repeat (matchbug_main (fun H =>
    repeat (matchbug_main (fun H' => check_not_equal H' H; progress (change H' with H)));
    let Hq := fresh "C" in hgeneralize_simpl H at 1 as Hq;
    try (clear H; intro; lazymatch goal with [ Hbot : _ |- _ ] => rename Hbot into H; revert H end)));
  simpl projT1 in *; simpl projT2 in *;
  matchbug_end.

Ltac Hgeneralize1 _ := Hgeneralize.

Internal Use : Hrevert

Ltac Hrevert delim :=
  repeat (match goal with [ Hcrr : _ |- _ ] => first [ check_equal Hcrr delim; fail 2 |
    first [ clear Hcrr | revert Hcrr ]
  ] end).

Internal Use : Hsimpl_with

Ltac Hsimpl_with simpl_tac tac :=
  let temp := fresh "_temp_" in
    assert (temp := I);
    Hgeneralize; try(tac); repeat (intro_eq; try (tac)); simpl_tac temp;
    clear_eq_upto temp; clear temp.

* Hsimpl

generalizes casts by Hgeneralize and then simplifies them by eliminating leading casts and composing composible casts

Lemma cast_intro : forall (U:Type) (Sig: U -> Type) (u:U) (a:Sig u) (v:U) (b:Sig v) (w:U) (H : u = w),
  {{ Sig # a == b }} -> {{ Sig # << Sig # H >> a == b }}.
intros until H. case H. auto.
Qed.

Lemma cast_intro_r : forall (U:Type) (Sig: U -> Type) (u:U) (a:Sig u) (v:U) (b:Sig v) (w:U) (H : v = w),
  {{ Sig # a == b }} -> {{ Sig # a == << Sig # H >> b }}.
intros until H. case H. auto.
Qed.

Lemma cast_compose: forall (U:Type) (Sig: U -> Type) (u:U) (a:Sig u) (v w:U) (H : u = v) (H' : v = w),
  << Sig # H' >> << Sig # H >> a = << Sig # trans_eq H H' >> a.
intros. case H'. case H. auto.
Qed.

Ltac Hsimpl := Hsimpl_with Hgeneralize1 ltac:(repeat (first [ apply cast_intro | apply cast_intro_r ]); repeat (rewrite cast_compose)).

* Hchange C1 with C2

change the cast C1 into C2 of the same type, using the UIP axiom, (which is equivalent to Streicher's Axiom K)

Tactic Notation "Hchange" constr(H1) "with" constr(H2) := (rewrite (UIP _ _ _ H1 H2); try (clear H1)).

* Hunify

unifies different casts of the same type

Ltac Hunify := (Hsimpl_with Hrevert
  ltac:(matchbug_begin;
        repeat (
          matchbug_main (fun H =>
          matchbug_main (fun H' =>
            check_not_equal H' H; (change H' with H || rewrite (UIP _ _ _ H' H)))));
        matchbug_end)).

* Hclear

clear identity casts

Definition idtemp := fun (A : Type) (x : A) => x.

Ltac Hclear_refl :=
  repeat (match goal with [ |- appcontext CTX [ @hcast _ ?Sig _ _ (@refl_equal _ ?w) ] ]
            => let G := context CTX [@idtemp (Sig w)] in change G; unfold idtemp end).

Ltac Hclear := Hsimpl; Hunify;
  Hsimpl_with Hgeneralize1 ltac:(matchbug_begin; repeat (matchbug_main (fun H => rewrite (UIP_refl _ _ H); Hclear_refl)); matchbug_end).

* Hrewrite ( <- ) H ( at occ )

given an Heq H : {{ Sig # t1 == t2 }}, it rewrite the (occ-th) and its dependent occurrences of t1 to << C >> t2 with an appropriate cast C.

Alternatively, one can use "(h)rewrite (Hrw H) ( at occ ); Hgeneralize". This allows the use of _ .

Definition Hty (U:Type) (Sig: U -> Type) (u:U) (a:Sig u) (v:U) (b:Sig v) (H: {{ Sig # a == b }}) : v = u := sym_eq (Heq_proj1 H).
Implicit Arguments Hty [U Sig u a v b].

Lemma Hrw: forall (U:Type) (Sig: U -> Type) (u v:U) (a:Sig u) (b:Sig v),
  forall H : {{ Sig # a == b }}, a = << Sig # Hty H >> b.
intros. Hsubst. rewrite (UIP _ _ _ _ (refl_equal _)). auto.
Qed.
Implicit Arguments Hrw [U Sig u a v b].

Ltac Hrewrite_with H rwtac :=
 (let H' := fresh "_temp_" in assert (H' := Hrw H); simpl in H'; rwtac H'; clear H'; Hgeneralize).

Tactic Notation "Hrewrite" constr(H) := (Hrewrite_with H ltac:(fun H' => rewrite H')).
Tactic Notation "Hrewrite" constr(H) "at" int_or_var(occ) := (Hrewrite_with H ltac:(fun H' => hrewrite H' at occ)).
Tactic Notation "Hhrewrite" constr(H) := (Hrewrite_with H ltac:(fun H' => hrewrite H')).
Tactic Notation "Hrewrite" "<-" constr(H) := (Hrewrite (sym_Heq H)).
Tactic Notation "Hrewrite" "<-" constr(H) "at" int_or_var(occ) := (Hrewrite (sym_Heq H) at occ).
Tactic Notation "Hhrewrite" "<-" constr(H) := (Hhrewrite (sym_Heq H)).

* Hrefl (T:Sig Pat) ( at occ )

replace the (occ-th) and its dependent occurrencies of T by << C >> T with the identity cast C.

one can also use "(h)rewrite (Hrf T) ( at occ ); Hgeneralize" especially when (s)he wants to use _ .

* Hreflrec (T:Sig Pat) ( at occ )

when the type of T is deeply dependent (i.e., deeper than depth 1), recursively apply Hrefl to T and its types to make it into the most general form.

Lemma Hrf: forall (U:Type) (Sig: U -> Type) (u:U) (a:Sig u), a = << Sig # refl_equal u >> a.
auto.
Qed.
Implicit Arguments Hrf [U].

Lemma HrfI: forall (A:HType) (a: A), a = <<< refl_equal A >>> a.
auto.
Qed.
Implicit Arguments HrfI [A].

Lemma Hrfgen: forall (U:Type) (Sig: U -> Type) (u:U) (a:Sig u), exists C, a = << Sig # C >> a.
intros. exists (refl_equal _). auto.
Qed.
Implicit Arguments Hrfgen [U].

Ltac Hrefl_with T rwtac :=
  let Hq := fresh "C" in let eqn := fresh "_temp_" in destruct (Hrfgen _ _ T) as [Hq eqn]; simpl in eqn; rwtac eqn; clear eqn; revert Hq.

Ltac Hreflrec_with T rwtac :=
 (Hrefl_with T rwtac;
  intro; lazymatch goal with [ Hcrr : ?eqn |- _ ] =>
    revert Hcrr;
    try (match eqn with
      | @eq _ _ (@existT _ ?Sig ?u ?X) => Hreflrec_with (X : Sig u) ltac:(fun eqn => hrewrite eqn at 2)
    end)
  end).

Tactic Notation "Hrefl" constr(T) := (Hrefl_with T ltac:(fun eqn => rewrite eqn); Hgeneralize).
Tactic Notation "Hrefl" constr(T) "at" int_or_var(occ) := (Hrefl_with T ltac:(fun eqn => hrewrite eqn at occ); Hgeneralize).
Tactic Notation "Hreflrec" constr(T) := (Hreflrec_with T ltac:(fun eqn => rewrite eqn); Hgeneralize).
Tactic Notation "Hreflrec" constr(T) "at" int_or_var(occ) := (Hreflrec_with T ltac:(fun eqn => hrewrite eqn at occ); Hgeneralize).

Tactic Notation "HreflI" constr(T) := (Hrefl (T : HId _)).
Tactic Notation "HreflI" constr(T) "at" int_or_var(occ) := (Hrefl (T : HId _) at occ).
Tactic Notation "HreflrecI" constr(T) := (Hreflrec (T : HId _)).
Tactic Notation "HreflrecI" constr(T) "at" int_or_var(occ) := (Hreflrec (T : HId _) at occ).

Internal Use : Hpop

Ltac Hpop H :=
  let temp := fresh "_temp_" in
    assert (temp := I);
    intros until H; lazymatch goal with [ Hbot : _ |- _ ] => move Hbot before temp; revert_eq_upto Hbot end;
    clear temp.

Internal Use : Hget

Ltac Hget H :=
 (intros until H;
  lazymatch goal with [ Hbot : _ |- _ ] => let Hnew := fresh in assert (Hnew := sym_eq Hbot) end;
  Hgeneralize).

Internal Use : Hsolve_with, Hsolve_hyps

Definition finish_tag := I.

Ltac Hsolve_with Hdelim tac_eq tac_Heq :=
 (Hgeneralize;
  Hlock_hyps_from_top_until 1 Hdelim; Hset_concl0;
  Hsubst;
  repeat (
    first [
      match goal with [ H := finish_tag |- _ ] => fail 2 end |

    
      let inv H :=
       (let temp := fresh "_temp_" in
        assert (temp:= I);
        inversion_eq_clear H; Hlock_hyps_from_bottom_upto 2 temp; try (Hlock_hyp 2 H);
        clear temp)
      in
      repeat (match goal with | [ H : @eq _ _ _ |- _ ] => inv H | [ H : @Heq _ _ _ _ _ _ |- _ ] => inv H end);
      Hunlock_hyps 2;
      Hsubst;

    
      let rewr tac Hcrr :=
       (move Hcrr before Hdelim; revert_eq_upto Hcrr;
        progress ( tac Hcrr );
        try (clear Hcrr);
        intro_eqs; Hgeneralize; Hsubst)
      in
      (match goal with
         | [ Hcrr : @eq _ _ _ |- _ ] => rewr tac_eq Hcrr
         | [ Hcrr : @Heq _ _ _ _ _ _ |- _ ] => rewr tac_Heq Hcrr
       end
      ||
      let finish := fresh "_temp_" in pose (finish := finish_tag))
  ]);
  try (match goal with [ H := finish_tag |- _ ] => clear H end);
  try (match goal with [ H : HeqLockHyp1 _ |- _ ] => try(move Hdelim after H) end);
  Hunlock_hyps 1; Hunset_concl0).

Tactic Notation "Hsolve_hyps_basic" hyp(Hdelim) := (Hsolve_with Hdelim ltac:(fun heq => rewrite heq) ltac:(fun heq => heq_rewrite heq)).

Tactic Notation "Hsolve_hyps" hyp(Hdelim) :=
 (Hsolve_with Hdelim
   ltac:(fun heq => first [ rewrite heq | hrewrite heq ])
   ltac:(fun heq => first [ heq_rewrite heq | heq_hrewrite heq | Hrewrite heq | Hhrewrite heq ])).

* Helim ( -> ) ( C )

try to turn the cast C (or the first cast when C is not given) into an identity cast by runnig the proof search engine

Ltac Helim_with H tac :=
 (let temp := fresh "_temp_" in
    assert (temp := I);
    Hpop H;
  let C := fresh "C" in
    lazymatch goal with [ Hbot : _ |- _ ] => rename Hbot into C end;
    revert_eq_upto temp;
    Hget C;
    tac temp;
    clear_eq_upto temp; clear temp).

Ltac Helim_basic H := Helim_with H ltac:(fun delim => Hsolve_hyps_basic delim).

Tactic Notation "Helim" ident(H) := (Helim_with H ltac:(fun delim => Hsolve_hyps delim)).
Tactic Notation "Helim" := (try (intro; lazymatch goal with [ H : _ |- _ ] => revert H; Helim H end)).
Tactic Notation "Helim" "->" ident(H) :=
 (Helim_with H ltac:(fun delim => lazymatch goal with [ Hbot : _ |- _ ] => apply sym_eq in Hbot end; Hsolve_hyps delim)).
Tactic Notation "Helim" "->" := (try (intro; lazymatch goal with [ H : _ |- _ ] => revert H; Helim -> H end)).

* Hgeteq ( -> ) C

obtain equations from the cast C. This is useful when one wants to simplify C by hand.

Tactic Notation "Hgeteq" ident(H) := (Helim_with H ltac:(fun delim =>
  lazymatch goal with [ Hnew : _ |- _ ] => inversion_eq_clear Hnew end;
  Hlock_hyps_from_top_until 1 delim; Hsubst; Hunlock_hyps 1; move delim at bottom)).

Tactic Notation "Hgeteq" "->" ident(H) := (Helim_with H ltac:(fun delim =>
  lazymatch goal with [ Hnew : _ |- _ ] => apply sym_eq in Hnew; inversion_eq_clear Hnew end;
  Hlock_hyps_from_top_until 1 delim; Hsubst; Hunlock_hyps 1; move delim at bottom)).

* Hsplit

split {{ Sig # a == b # x == y }} into two subgoals x = y and {{{ a == b }}}, which is equivalent to JMeq a b (see the lemma Heq_JMeq).

Ltac Hsplit := intro_eqs; apply Heq_split; Hsimpl.

* Hsimpl_hyps

performes the following simplification in all hyps
  • {{ Sig # << C >> a == b }} -> {{ Sig # a == b }}
  • {{ Sig # a == << C >> b }} -> {{ Sig # a == b }}

Lemma cast_elim : forall (U:Type) (Sig: U -> Type) (u:U) (a:Sig u) (v:U) (b:Sig v) (w:U) (H : u = w),
  {{ Sig # << Sig # H >> a == b }} -> {{ Sig # a == b }}.
intros until H. case H. auto.
Qed.

Lemma cast_elim_r : forall (U:Type) (Sig: U -> Type) (u:U) (a:Sig u) (v:U) (b:Sig v) (w:U) (H : v = w),
  {{ Sig # a == << Sig # H >> b }} -> {{ Sig # a == b }}.
intros until H. case H. auto.
Qed.

Ltac Hsimpl_hyps :=
  repeat (match goal with [H : @Heq _ _ _ _ _ _ |- _] => progress (repeat (first [ apply cast_elim in H | apply cast_elim_r in H ])) end).

Tactics followed by Helim and Hclear.

* Helimc
Tactic Notation "Helimc" ident(H) := (Helim H; Hclear).
Tactic Notation "Helimc" := (Helim; Hclear).
Tactic Notation "Helimc" "->" ident(H) := (Helim -> H; Hclear).
Tactic Notation "Helimc" "->" := (Helim ->; Hclear).

* hrewritec
Tactic Notation "hrewritec" constr(eqn) "at" int_or_var(occ) := (hrewrite eqn at occ; try (clear eqn); Hclear).
Tactic Notation "hrewritec" "<-" constr(eqn) "at" int_or_var(occ) := (hrewrite <- eqn at occ; try (clear eqn); Hclear).
Tactic Notation "hrewritec" constr(eqn) := (hrewrite eqn; try (clear eqn); Hclear).
Tactic Notation "hrewritec" "<-" constr(eqn) := (hrewrite <- eqn; try (clear eqn); Hclear).

* heq_hrewritec
Tactic Notation "heq" "hrewritec" constr(eqn) "at" int_or_var(occ) := (heq_hrewrite eqn at occ; try (clear eqn); Hclear).
Tactic Notation "heq" "hrewritec" "<-" constr(eqn) "at" int_or_var(occ) := (heq_hrewrite <- eqn at occ; try (clear eqn); Hclear).
Tactic Notation "heq" "hrewritec" constr(eqn) := (heq_hrewrite eqn; try (clear eqn); Hclear).
Tactic Notation "heq" "hrewritec" "<-" constr(eqn) := (heq_hrewrite <- eqn; try (clear eqn); Hclear).

* Hrewritec
Tactic Notation "Hrewritec" constr(H) := ((Hrewrite H); Helimc).
Tactic Notation "Hrewritec" "<-" constr(H) := ((Hrewrite <- H); Helimc).
Tactic Notation "Hrewritec" constr(H) "at" int_or_var(occ) := ((Hrewrite H at occ); Helimc).
Tactic Notation "Hrewritec" "<-" constr(H) "at" int_or_var(occ) := ((Hrewrite <- H at occ); Helimc).

* Hsimplc
Ltac Hsimplc := Hsimpl; Helimc.

Useful lemmas


Require Import FunctionalExtensionality.

Lemma Heq_ind_gen: forall (U:Type) (Sig: U -> Type) (P: forall u, Sig u -> Prop) u (a:Sig u) v (b:Sig v),
  P _ a -> {{ Sig # a == b }} -> P _ b.
intros. Hsubst. auto.
Qed.

Lemma Heq_extensionality: forall (U:Type) (A:Type) (Sig: U -> Type) (Sig': U -> Type) (F: forall u, (A -> Sig u) -> Sig' u)
  u u' (P: A -> Sig u) (P': A -> Sig u'),
  (u = u' \/ exists a:A, True) -> (forall a, {{ Sig # P a == P' a }}) -> {{ Sig' # F u P == F u' P' }}.

intros. assert (u = u'). destruct H; auto. destruct H. specialize H0 with x. Hsubst. auto.
Hsubst. replace P with P'. auto. extensionality a. apply (Heq_eq Sig). auto.
Qed.
Implicit Arguments Heq_extensionality [U A u u'].

Lemma Hfundep: forall (A A':Type) (P:A->Type) (P':A'->Type) (opr: forall a:A, P a) (opr': forall a': A', P' a'),
  A = A' -> (forall a a', {{{ a == a' }}} -> {{{ opr a == opr' a' }}}) -> {{{ opr == opr' }}}.
intros. Hsubst.
assert (P = P'). extensionality v. eapply (@Heq_proj1 _ HId). apply (H0 v v). auto.
Hsubst. apply eq_Heq. extensionality v. apply (Heq_eq HId). apply H0. auto.
Qed.
Implicit Arguments Hfundep [A A' P P'].

Lemma Happdep: forall (A A':Type) (P:A->Type) (P':A'->Type) (opr: forall a:A, P a) (opr': forall a': A', P' a') a a',
  {{{ P == P' }}} -> {{{ a == a' }}} -> {{{ opr == opr' }}} -> {{{ opr a == opr' a' }}}.
intros. Hsubst. auto.
Qed.
Implicit Arguments Happdep [A A' P P'].

Lemma Hfun: forall (A A' B B':Type) (opr: A -> B) (opr': A' -> B'),
  A = A' -> (forall a a', {{{ a == a' }}} -> {{{ opr a == opr' a' }}}) -> {{{ opr == opr' }}}.
intros. apply Hfundep; auto.
Qed.
Implicit Arguments Hfun [A A' B B'].

Lemma Happ: forall (A A' B B':Type) (opr: A -> B) (opr': A' -> B') a a',
  B = B' -> {{{ a == a' }}} -> {{{ opr == opr' }}} -> {{{ opr a == opr' a' }}}.
intros. Hsubst. auto.
Qed.
Implicit Arguments Happ [A A' B B'].