Why does `Hint Resolve X` fail, where` let: X` works?

Here is a logic puzzle about the self-referential sentences I am trying to automate in Coq. The goal is to prove P1

. I am also using the LibTactics library from Software Foundations.

Require Import List.
Import ListNotations.
Require Import LibTactics. 

Inductive symbol : Type := | P | Q | P' | Q'.

Definition sentence : Type := list symbol.

Variable true : sentence -> Prop.

Variable provable : sentence -> Prop.

Hypothesis HQ'1 : forall (X : sentence), true (Q' :: X) -> ~ provable (X ++ X).
Hint Resolve HQ'1.

Hypothesis HQ'2 : forall (X : sentence), ~ provable (X ++ X) -> true (Q' :: X).
Hint Resolve HQ'2.

Hypothesis HC : forall (X : sentence), provable X -> true X.
Hint Resolve HC.

Theorem P1 : 
true [Q';Q'] /\ ~ provable [Q';Q'].

      

The following solution works, but seems unnecessarily long:

Theorem P1 : 
true [Q';Q'] /\ ~ provable [Q';Q'].
lets : HQ'1. lets : HQ'2. lets : HC.  
jauto. Qed.

      

From what I understand, adding X

to context lets : X

is just one way to make the lemma X

available to auto. As I already added HQ'1

, HQ'2

and HC

for the database hint with help Hint Resolve

, everything lets

in the above solution is redundant and the following should also work:

Theorem P1 : 
true [Q';Q'] /\ ~ provable [Q';Q'].
jauto. Qed.

      

But this is not the case. What's the difference between them? Does Coq contain hypotheses in context and database clues differently?

+1
coq


source to share


No one has answered this question yet

See similar questions:

3
Can't automate lemme that works manually in Coq

or similar:

6
Why does Coq.Init.Logic define "A & # 8594; B"?
6
Couldn't use let-destruct on tuple in Coq
4
Why does "intuition" work with Coq?
3
Screen resolution and autoplay
2
Why is this rewriting not done in the context of dependent types
2
Induction hypothesis for free closed term variables in simply typed lambda calculus
1
Why doesn't semicolon proof work with periods?
1
Why is unwrapping not working for lt (less) in Coq?
1
"overwrite to" fails when "overwrite" works
0
Coq - disj_conj_intro_patterns for inductive sentences



All Articles
Loading...
X
Show
Funny
Dev
Pics