Skip to content

GitLab

Closed
Created by DAILLER Sylvain@sdaillerDeveloper

Add a transformation destruct*

Add a transformation that performs destruct recursively on an hypothesis. It should handle all currently handled constructs: disjunction, conjunction, implications.

predicate p1
predicate p2
predicate p3

axiom H: p1 -> p2 -> p3
goal G: 1 = 1

destruct H should produce 3 new goals for p1, p2 and H : p3 |- G ? [EDIT: To be more clear]

This should produce 3 new subgoals which are the following:

  predicate p1
  predicate p2
  predicate p3
  
  goal G : p1
  predicate p1
  predicate p2
  predicate p3
  
  goal G : p2
  predicate p1
  predicate p2
  predicate p3
  
  axiom H : p3
  goal G : 1 = 1

Sorry for the misleading notations.

Edited by DAILLER Sylvain
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information