Executable Specification

[View str1.sig] [View str1.mod]
sig str1.

type   p, q, r          o.
module str1.

r :- (p => q) => r.
r :- q.

Reasoning

[View str1.thm]

Click on a command or tactic to see a detailed view of its use.

Specification "str1".

Define ctx : olist -> prop by
  ctx nil;
  ctx ((p => q) :: L) := ctx L.

Theorem ctx_mem : forall L E,
  ctx L -> member E L -> E = (p => q).

%% This lemma is NOT provable since r depends on q 
%% which in turn depends on p. 
Theorem indep : 
   (forall L,
      ctx L -> {L, p |- p} -> {L |- p})
/\ (forall L,
      ctx L -> {L, p |- q} -> {L |- q})
/\ (forall L,
      ctx L -> {L, p |- r} -> {L |- r}).
induction on 2 2 2. intros. split. % p is independent of p (which is NOT provable) intros. case H2. case H4. case H3. skip. % Cannot proceed apply ctx_mem to _ H5. case H3. % p is independent of q (again, not provable) intros. case H2. case H4. case H3. apply ctx_mem to _ H5. case H3. % application of IH which is not provable apply IH to _ H6. search. % p is independent of r (not provable) intros. case H2. apply IH2 to _ H3. search. % application of IH1 which is not provable apply IH1 to _ H3. search. case H4. case H3. apply ctx_mem to _ H5. case H3.