Library Equations.NoConfusion


Instances of NoConfusion for the standard datatypes. To be used by equations when it needs applications of injectivity or discrimination on some equation.

Require Import Coq.Program.Tactics Bvector List.
Require Import Equations.Signature Equations.EqDec Equations.Constants.
Require Export Equations.DepElim.

Ltac noconf H ::=
  blocked ltac:(noconf_ref H; simplify_dep_elim) ; auto 3.

Used by the Derive NoConfusion command.

Ltac destruct_sigma id :=
  match type of id with
    @sigma ?A ?P => let idx := fresh "idx" in
                   destruct id as [idx id];
                     repeat destruct_sigma idx; simpl in id
                                                         
  | _ => idtac
  end.

Ltac solve_noconf_prf := intros;
  on_last_hyp ltac:(fun id => destruct id) ;
  on_last_hyp ltac:(fun id =>
                      destruct_sigma id;
                      elim id) ;
  constructor.

Ltac destruct_tele_eq H :=
  match type of H with
    ?x = ?y =>
    let rhs := fresh in
    set (rhs := y) in *; pattern sigma rhs; clearbody rhs;
    destruct H; simpl
  end.

Ltac solve_noconf_inv := intros;
  match goal with
    |- ?R ?a ?b => destruct_sigma a; destruct_sigma b;
                   destruct a ; depelim b; simpl in * |-;
                 on_last_hyp ltac:(fun id => hnf in id; destruct_tele_eq id || destruct id);
                 solve [constructor]
  end.

Ltac solve_noconf_inv_equiv :=
  intros;
  
  on_last_hyp ltac:(fun id => destruct id) ;
  
  on_last_hyp ltac:(fun id => destruct_sigma id; elim id) ;
  simpl; constructor.

Ltac solve_noconf := simpl; intros;
    match goal with
      [ H : @eq _ _ _ |- @eq _ _ _ ] => try solve_noconf_inv_equiv
    | [ H : @eq _ _ _ |- _ ] => try solve_noconf_prf
    | [ |- @eq _ _ _ ] => try solve_noconf_inv
    end.

Ltac solve_noconf_hom := simpl; intros;
    match goal with
      [ H : @eq _ _ _ |- @eq _ _ _ ] => try solve_noconf_inv_equiv
    | [ H : @eq _ _ _ |- _ ] => try solve_noconf_prf
    | [ |- @eq _ _ _ ] => try solve_noconf_inv
    end.

Derive NoConfusion for unit bool nat option sum Datatypes.prod list sigT sig.

Extraction Inline noConfusion NoConfusionPackage_nat.