title: What tactic should I use to avoid stucking in endless loop, in Coq?
body: <p>I cannot solve a Coq Theorem where I should use denotational semantics. If I go forward from this point I am always stucking in an endless loop.</p>
  <p>What tactic should be used in this case? Where did I go wrong with this one? Should I start differently?</p>
  <pre><code>From Coq Require Import Strings.String
                          Arith.PeanoNat
                          Arith.Plus.
  
  Definition Ident : Type := string.
  
  Inductive AExp : Type :=
  | ALit (n : nat)
  | AVar (s : Ident)
  | APlus (a1 a2 : AExp)
  | ADup (n : AExp)
  .
  
  Definition State := Ident -&gt; nat.
  
  Definition empty : State := fun x =&gt; 0.
  
  Definition aState : State := 
  fun x =&gt;
    match x with
    | &quot;X&quot;%string =&gt; 1
    | &quot;Y&quot;%string =&gt; 2
    | &quot;Z&quot;%string =&gt; 42
    | _ =&gt; 0
    end
  .
  
  Definition X:Ident := &quot;X&quot;%string.
  Definition Y:Ident := &quot;Y&quot;%string.
  Definition Z:Ident := &quot;Z&quot;%string.
  
  Fixpoint val (a : AExp) (s : State) : nat :=
  match a with
  | ALit n =&gt; n
  | AVar x =&gt; s x
  | APlus a1 a2 =&gt; val a1 s + val a2 s
  | ADup a =&gt; val a s + val a s
  end.
  
  Fixpoint aqb (a1 a2 : AExp) : bool :=
  match a1, a2 with
  | ALit n, ALit m =&gt; Nat.eqb n m
  | AVar s, AVar x =&gt; String.eqb s x
  | APlus a1 a2, APlus a1' a2' =&gt; aqb a1 a1' &amp;&amp; aqb a2 a2'
  | ADup a1, ADup a1' =&gt; aqb a1 a1'
  | _, _ =&gt; false
  end.
  
  Fixpoint optmal (a : AExp) : AExp :=
  match a with
  | APlus a1 a2 =&gt; 
    if aqb a1 a2
    then ADup (optmal a1)
    else APlus (optmal a1) (optmal a2)
  | ADup a0 =&gt; ADup (optmal a0)
  | _ =&gt; a
  end.
  
  Theorem optmald :
    forall a s, val a s = val (optmal a) s.
  Proof.
  intros. unfold val. induction a.
  * simpl. reflexivity.
  * simpl. reflexivity.
  * 
  
  </code></pre>