Title: Theory / Unimportant / CS / Programming / Coq / ltac
Tags: FromInstruction algoToProg computer_to_instruction hasNotNewEffectReturnsMeaning some_instruction todo_declaration

Instruction: Admitted
Page: https://softwarefoundations.cis.upenn.edu/current/lf-current/Basics.html
Effect: Placeholder for incomplete proof
Language: coq
Chapter: FUNCTIONAL PROGRAMMING IN COQ
Extra: prog

Instruction: Check foo
Page: https://softwarefoundations.cis.upenn.edu/current/lf-current/Basics.html
Effect: Print the type of foo
Language: coq
Chapter: FUNCTIONAL PROGRAMMING IN COQ
Extra: prog

Instruction: Intros foo_1 ... foo_n.
Page: https://softwarefoundations.cis.upenn.edu/current/lf-current/Basics.html
Effect: The n first universally quantified variables and hypothesis are now named foo_i and are removed from the goal
Language: coq
Chapter: FUNCTIONAL PROGRAMMING IN COQ
Extra: prog

Instruction: rewrite -> H
Page: https://softwarefoundations.cis.upenn.edu/current/lf-current/Basics.html
Effect: Replace foo in the goal by bar
Language: coq
Chapter: FUNCTIONAL PROGRAMMING IN COQ
Variables: H is an equality of the form foo = bar
Extra: prog

Instruction: rewrite <- foo = bar
Page: https://softwarefoundations.cis.upenn.edu/current/lf-current/Basics.html
Effect: Replace bar in the goal by foo
Language: coq
Chapter: FUNCTIONAL PROGRAMMING IN COQ
Extra: prog

Instruction: Abort
Page: https://softwarefoundations.cis.upenn.edu/current/lf-current/Basics.html
Effect: Abort the current proof and the Theorem being proved
Language: coq
Chapter: FUNCTIONAL PROGRAMMING IN COQ
Extra: prog

Instruction: destruct foo as [bar_1,1 ... bar_1,n_1|...|bar_m,1 ... bar_m,n_m]
Page: https://softwarefoundations.cis.upenn.edu/current/lf-current/Basics.html
Effect: create m subgoals, in the i-th subgoal, foo is assumed to be equal to C_i(bar_i,1 ... bar_i,n_m)
Language: coq
Chapter: FUNCTIONAL PROGRAMMING IN COQ
Variables: foo a variable of inductive type with m constructors C_i taking n_i arguments each
Extra: prog

Instruction: Compute (foo)
Page: https://softwarefoundations.cis.upenn.edu/current/lf-current/Basics.html
Effect: Evaluate foo and return its value
Language: coq
Chapter: FUNCTIONAL PROGRAMMING IN COQ
Extra: prog

Instruction: unfold foo
Page: 24
Effect: unfold foo at 0
Language: coq
Chapter: 2
Section: 1.4

Instruction: unfold foo at n
Page: 24
Effect: replace the n-th occurrence of foo by its definition
Language: coq
Chapter: 2
Section: 1.4

Instruction: fold foo
Page: 25
Effect: find a place where foo 's definition is present and replace it by foo
Language: coq
Chapter: 2
Section: 1.4

Instruction: reflexivity.
Page: 25
Effect: normalize the term of the current goal and check they are equal
Language: coq
Chapter: 2
Section: 1.4
Assuming: current goal is an equality

Instruction: tactic1; tactic2
Page: 28
Effect: apply tactic1. Apply tactic2 to each subgoal of tactic1
Language: ltac
Chapter: 2
Section: 1.4

Instruction: Qed.
Page: 25
Effect: Check that the proof is finished and, if so, saves it
Language: ltac
Chapter: 2
Section: 1.4

Instruction: rewrite (foo (expr))
Page: 29
Effect: apply rewrite rule foo on the subterm expr of the current goal
Language: coq
Chapter: 2
Section: 1.4

Instruction: Hint Rewrite foo.
Page: 37
Effect: Uses rule foo when applying automated proof search
Chapter: 2

Instruction: destruct foo
Page: 41
Effect: Start a proof by case on the different possible values of foo
Language: coq
Chapter: 3
Section: 1

Question: Difference between `destruct foo` and `induction foo`
Answer: `destruct` do not introduce induction hypothesis on the subpart of foo
Page: 41
Chapter: 3
Section: 1

Instruction: discriminate
Page: 45
Effect: validate that a != b if a and b uses distinct constructors
Language: coq
Chapter: 3
Section: 1

Instruction: injection
Page: 45
Language: coq
Chapter: 3
Returns: replace
Constructor arg1 ... argn = Constructor arg1' ... argn'
by
arg1 = arg1'
...
argn = argn'

Instruction: Argument Constructor [arg]
Page: 45
Effect: When Constructor is used, infer a value for arg automatically
Language: coq
Chapter: 3

Instruction: Section section_name.
  Variable value_1 : Type_1.
  ...
  Variable value_n : Type_n.
  foo
End section_name.
Page: 45
Effect: foo is interpreted as usual, with value_i some value of type Type_i.
Outside of the section, all values defined in foo takes n extra arguments value_1, ..., value_n
Language: coq
Chapter: 3

Instruction: Variable value : Type.
Page: 50
Meaning: In the current section, there is a constant value of type Type. Outside of it it is an extra argument to all section's definition
Language: coq
Chapter: 3
Section: 4
Scope: Until the end of the innermost section