Ssreflect Users Discussion List

[Sean McLaughlin <>]

Dear ssreflect experts,

  I was wondering how to achieve an effect similar to 'dependent induction' with ssreflect. Suppose you have the following small sequent calculus:



(*********************************************************)

Require Import ssreflect ssrbool ssrfun eqtype ssrnat fintype finset seq.

Require Import Coq.Program.Equality. (* For dependent induction. *) 

Set Implicit Arguments.

Unset Strict Implicit.

Import Prenex Implicits.

Inductive prop : Type :=

| Atom : nat -> prop

| And : prop -> prop -> prop

.

Notation "a ∧ b" := (And a b) (at level 49).

Fixpoint eqn (m n : prop) {struct m} : bool :=

  match m, n with

    | Atom p1, Atom p2 => p1 == p2

    | A1 ∧ B1, A2 ∧ B2 => eqn A1 A2 && eqn B1 B2

    | _, _ => false

  end.

Lemma eqn_refl : forall p, eqn p p.

Proof.

  elim => [s|m H1 n H2] //; try apply/andP => //.

  exact (eq_refl _).

Qed.

Lemma eqnP : Equality.axiom eqn.

Proof.

  move=> n m; apply: (iffP idP) => [|<-]; last by exact (eqn_refl _).

  move: m; elim: n; try by elim.

  - move=> s; case; try by rewrite /=.

  move=> s1 /= H.

  by rewrite (eqP H).

  - move=> m Hm n Hn k.

  case k; try by rewrite /=.

  move=> m1 m2 /=.

  move/andP=> [H1 H2].

  by rewrite (Hm _ H1) (Hn _ H2).

Qed.

Canonical Structure prop_eqMixin := EqMixin eqnP.

Canonical Structure prop_eqType := Eval hnf in EqType prop_eqMixin.

Definition Ctx := seq_eqType prop_eqType.

Structure Seq : Type := mkSeq { ants  : Ctx ; cons  : prop }.

Notation "Γ ⊢ γ" := (mkSeq Γ γ) (at level 80).

Inductive SC : Seq -> Prop :=

| Init : forall p Γ,

  SC (Atom p :: Γ ⊢ Atom p) 

| AndR : forall A B Γ,

  SC (Γ ⊢ A) ->

  SC (Γ ⊢ B) ->

  SC (Γ ⊢ A ∧ B)

| AndL1 : forall A B Γ γ,

  SC (A :: Γ ⊢ γ) ->

  SC (A ∧ B :: Γ ⊢ γ)

| AndL2 : forall A B Γ γ,

  SC (B :: Γ ⊢ γ) ->

  SC (A ∧ B :: Γ ⊢ γ)

| Exchange : forall Γ1 Γ2 γ,

  SC (Γ1 ⊢ γ) ->

  perm_eq Γ1 Γ2 ->

  SC (Γ2 ⊢ γ)

.

(*********************************************************)

Then we want to prove weakening, so we try:

Lemma Weaken : forall p Γ γ, SC (Γ ⊢ γ) -> SC (p :: Γ ⊢ γ).

Proof.

move=> p Γ γ.

Now, elim doesn't work here, as it fails to equate the context in the assumption list and the one in the goal.  There's a tactic that does close to what I want: 

move=> H; dependent induction H.

I just wonder if there's a way to use ssreflect.  dependent induction invents names for all the generated variables and creates equalities that are a bit cumbersome.  I tried to follow section 5.6 (Type Familes) of the tutorial, but I couldn't get it to work.

Thanks!

Sean