Ssreflect Users Discussion List

[Georges Gonthier <>]

  Hi Sean,

 

   Ssreflect provides roughly the functionality of inversion/dependent elim, but in kit form. You need to generate an equation for the variable that will be substituted by elim, which you can then decompose using injection (which ssreflect conveniently maps to the [..] intro pattern), and rewrite either immediately (using ->) or later at your convenience.

  Here you need to create an equation involving induction parameters (Γ  and γ) so you cannot use the equation generation mechanism of elim; you must create the equation beforehand with move:

 

    move=> p Γ γ;  move def_s: (Γ ⊢ γ)  => s SCs; move: SCs Γ γ def_s.

   elim: s / => [p Γ | A B Γ _ IH_A _ IH_B | A B  Γ γ _ IH | A B  Γ γ _ IH |  Γ1 Γ2 γ _ IH perm12] _ _ [-> ->].

 

I prefer to try to keep the intro pattern together, but with a bigger inductive you might need to  split it into separate calls to move.

 

 In this case, you can also make the problem go away by not using the Seq type in the definition of SC, and having two separate family parameters Γ and γ – this tells Coq to substitute Γ and γ independently.

 

  Best,

  Georges

 

(I’m cc’ing the ssreflect list, which I think you meant to do).

 

From: Sean McLaughlin [mailto:]
Sent: 20 April 2010 00:34
To: Georges Gonthier
Subject: dependent elim?

 

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