Logic and Semantics of Programming languages

In this repository I will try to formalize most of the proofs from my Logic and Semantics course in University at RPTU.

Each week a new assignment is given which may or may not depend on each other.

Usage of Lia and other auto solvers

Since this is supposed to teach me how to use Coq I try to avoid using lia, auto, omega and what not. But when I use these tactics there could be several reasons for it:

• The theorem/lemma which is to proof should be in the standard lib and I cannot find it or there is some other way unkown to me.
• The theorem/lemma which is to proof is to hard for me and I don't understand how to solve it.
• In generall I will use it when I don't see another way to solve this and it is not a major theorem.