This question is related to a strategic game (bargaining, protocol, crypto,...) setting I investigate during holidays where players are Coq users.
Some of them have limited reasoning capabilities such as for example being only able to intro and apply an hypothesis or a lemma they were given.
Some others may have access to tauto.
In contrast, some rational players have unlimited reasoning capabilities and know other players’ type. Rational players can therefore reflect on what other players can prove or not and build their decision on it for their next move in the game.
Non-rational players have never access to CIC terms. I therefore restrict their Ltac grammar to a consistent but smaller fragment. I also restrict their list of atomic tactics. For example I would not allow a variant of apply with patterns or other which opens the door to CIC terms.
In the case of this question, it is simply a finite sequence of vanilla intro and apply tactics separated by a dot.
To summarize, a player’s type is defined by an Ltac grammar subset, a list of atomic tactics and a bag of lemmas given at the start of the game.
Here is the most verbose (smallest steps) proof of a tautology :
Lemma Or_commutative : forall P Q : Prop, P \/ Q -> Q \/ P.
Proof.
intro P.
intro Q.
intro H.
elim H.
intro HP.
right.
apply HP.
intro HQ.
left.
apply HQ.
Qed.
It is clear that we need elim, right and left tactics. Intro and apply are not sufficient.
Question : how can I prove that she cannot prove Or_commutative with only intro and apply ?
Goal cannot_prove_or_commutative_with_IAs : ????
Proof.
(* Here I want to show that no sequence of
vanilla intro and apply tactics can solve the goal*)
(* I may define a structure of proof that is a sequence of intro and apply
and show that after step 3, it will fail or will not change the judgment.
How would I do that ? *)
(* Or should I go to the definitions of intro an apply and show that they cannot
handle OR terms ? *)
(* Or should I investigate plugins to reflect on tactics ? I heard of Mtac2 recently *)
Qed.