CODEWITHSUNDEEP
coqcoq-tactic
Sara
Sara

Reputation: 339

How to use a tactic with a hypothesis in Coq?

I'm new in Coq and I have run into a dead end. I have a inductive definition that looks roughly like this (I have defined accept inductively before) :

Inductive fun : accepts -> Prop :=
  | fn1 : fun True
  | fn2 : forall (n : nat )(A : accepts), fun A -> fun (n A).

What I need to prove is this:

Lemma lem_1  (A : formula) (n : nat) (h : fun (n A)) : fun A.

Of course, at starting the proof I get 

 A : accepts
 n : nat
 h : fun (n A)
 ============================
 fun A

I have spent a long time reading about tactics, trying to find some way to be able to plug h into my fn2 or something like that, and I just can't find a way to do that. Can someone please guide me here and give me some idea?? I've also tried doing something to simplify fun A into A but I have not succeeded there either. Thank you very much for your help!

Upvotes: 0

Views: 676

Answers (1)

Arthur Azevedo De Amorim
Arthur Azevedo De Amorim

Reputation: 23582

It seems that you want to argue that your h hypothesis was produced using the fn2 rule. In Coq jargon, this requires inverting that hypothesis. To do that, you can call inversion h. Applying is the opposite process: combining the fn2 rule with a hypothesis that states fun A to derive fun (n A).

Upvotes: 1

Related Questions