search

epfl-lara / lisa

Proof assistant based on first-order logic and set theory
Apache License 2.0
33 stars 18 forks source link

Restricted function theorems #164

Closed dhalilov closed 1 year ago

dhalilov commented 1 year ago

Description

This PR proves several theorems regarding restricted functions. Notably, it proves the relation domain of a restricted function

relationDomain(restrictedFunction(f, x)) === setIntersection(x, relationDomain(f))

as well as a cancellation theorem:

restrictedFunction(f, relationDomain(f)) === f

that is useful for group theory.

It also contains several tactics imported from the Work-in-Progress on Group Theory (#151), as well as first-order logic lemmas for proving the theorem.

Note that since Definition tactic uses Tautology, I placed the tactics in the main submodule instead of SimpleDeducedSteps.