Subset.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Tactics related to subsets and proof irrelevance.

Require Import Coq.Program.Utils.
Require Import Coq.Program.Equality.
Require Export ProofIrrelevance.

Local Open Scope program_scope.

The following tactics implement a poor-man's solution for proof-irrelevance: it tries to factorize every proof of the same proposition in a goal so that equality of such proofs becomes trivial.

Ltac on_subset_proof_aux tac T :=
  match T with
    | context [ exist ?P _ ?p ] => try on_subset_proof_aux tac P ; tac p
  end.

Ltac on_subset_proof tac :=
  match goal with
    [ |- ?T ] => on_subset_proof_aux tac T
  end.

Ltac abstract_any_hyp H' p :=
  match type of p with
    ?X =>
    match goal with
      | [ H : X |- _ ] => fail 1
      | _ => set (H':=p) ; try (change p with H') ; clearbody H'
    end
  end.

Ltac abstract_subset_proof :=
  on_subset_proof ltac:(fun p => let H := fresh "eqH" in abstract_any_hyp H p ; simpl in H).

Ltac abstract_subset_proofs := repeat abstract_subset_proof.

Ltac pi_subset_proof_hyp p :=
  match type of p with
    ?X =>
    match goal with
      | [ H : X |- _ ] =>
        match p with
          | H => fail 2
          | _ => rewrite (proof_irrelevance X p H)
        end
      | _ => fail " No hypothesis with same type "
    end
  end.

Ltac pi_subset_proof := on_subset_proof pi_subset_proof_hyp.

Ltac pi_subset_proofs := repeat pi_subset_proof.

The two preceding tactics in sequence.

Ltac clear_subset_proofs :=
  abstract_subset_proofs ; simpl in * |- ; pi_subset_proofs ; clear_dups.

Ltac pi := repeat f_equal ; apply proof_irrelevance.

Lemma subset_eq : forall A (P : A -> Prop) (n m : sig P), n = m <-> `n = `m.forall (A : Type) (P : A -> Prop)
  (n m : {x : A | P x}), n = m <-> ` n = ` m
Proof.forall (A : Type) (P : A -> Prop)
  (n m : {x : A | P x}), n = m <-> ` n = ` m
  destruct n as (x,p).A:Type
P:A -> Prop
x:A
p:P x
forall m : {x : A | P x},
exist P x p = m <-> ` (exist P x p) = ` m
  destruct m as (x',p').A:Type
P:A -> Prop
x:A
p:P x
x':A
p':P x'
exist P x p = exist P x' p' <->
` (exist P x p) = ` (exist P x' p')
  simpl.A:Type
P:A -> Prop
x:A
p:P x
x':A
p':P x'
exist P x p = exist P x' p' <-> x = x'
  split ; intros ; subst.A:Type
P:A -> Prop
x:A
p:P x
x':A
p':P x'
H:exist P x p = exist P x' p'
x = x'
A:Type
P:A -> Prop
x':A
p, p':P x'
exist P x' p = exist P x' p'

  -A:Type
P:A -> Prop
x:A
p:P x
x':A
p':P x'
H:exist P x p = exist P x' p'
x = x' inversion H.A:Type
P:A -> Prop
x:A
p:P x
x':A
p':P x'
H:exist P x p = exist P x' p'
H1:x = x'
x' = x'
    reflexivity.

  -A:Type
P:A -> Prop
x':A
p, p':P x'
exist P x' p = exist P x' p' pi.
Qed.

(* Somewhat trivial definition, but not unfolded automatically hence we can match on [match_eq ?A ?B ?x ?f]
   in tactics. *)

Definition match_eq (A B : Type) (x : A) (fn : {y : A | y = x} -> B) : B :=
  fn (exist _ x eq_refl).

(* This is what we want to be able to do: replace the originally matched object by a new,
   propositionally equal one. If [fn] works on [x] it should work on any [y | y = x]. *)

Lemma match_eq_rewrite : forall (A B : Type) (x : A) (fn : {y : A | y = x} -> B)
  (y : {y:A | y = x}),
  match_eq A B x fn = fn y.forall (A B : Type) (x : A)
  (fn : {y : A | y = x} -> B) (y : {y : A | y = x}),
match_eq A B x fn = fn y
Proof.forall (A B : Type) (x : A)
  (fn : {y : A | y = x} -> B) (y : {y : A | y = x}),
match_eq A B x fn = fn y
  intros.A, B:Type
x:A
fn:{y0 : A | y0 = x} -> B
y:{y0 : A | y0 = x}
match_eq A B x fn = fn y
  unfold match_eq.A, B:Type
x:A
fn:{y0 : A | y0 = x} -> B
y:{y0 : A | y0 = x}
fn (exist (fun y0 : A => y0 = x) x eq_refl) = fn y
  f_equal.A, B:Type
x:A
fn:{y0 : A | y0 = x} -> B
y:{y0 : A | y0 = x}
exist (fun y0 : A => y0 = x) x eq_refl = y
  destruct y.A, B:Type
x:A
fn:{y : A | y = x} -> B
x0:A
e:x0 = x
exist (fun y : A => y = x) x eq_refl =
exist (fun y : A => y = x) x0 e
  (* uses proof-irrelevance *)
  apply <- subset_eq.A, B:Type
x:A
fn:{y : A | y = x} -> B
x0:A
e:x0 = x
` (exist (fun y : A => y = x) x eq_refl) =
` (exist (fun y : A => y = x) x0 e)
  symmetry.A, B:Type
x:A
fn:{y : A | y = x} -> B
x0:A
e:x0 = x
` (exist (fun y : A => y = x) x0 e) =
` (exist (fun y : A => y = x) x eq_refl) assumption.
Qed.

Now we make a tactic to be able to rewrite a term t which is applied to a match_eq using an arbitrary equality t = u, and u is now the subject of the match.

Ltac rewrite_match_eq H :=
  match goal with
    [ |- ?T ] =>
    match T with
      context [ match_eq ?A ?B ?t ?f ] =>
      rewrite (match_eq_rewrite A B t f (exist _ _ (eq_sym H)))
    end
  end.

Otherwise we can simply unfold match_eq and the term trivially reduces to the original definition.

Ltac simpl_match_eq := unfold match_eq ; simpl.